-
Notifications
You must be signed in to change notification settings - Fork 12
/
student.html
executable file
·130 lines (123 loc) · 4.62 KB
/
student.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="Cache-Control" content="no-cache">
<title>Lurch</title>
<meta name="viewport" content="width=device-width, initial-scale=1">
<script type="module" src="lurchmath/editor.js"></script>
<script type="module" src="lde/src/experimental/lde-debug.js"></script>
<link rel="shortcut icon" href="lurchmath/favicon.ico">
<link rel="stylesheet" href="lurchmath/main-app-styles.css">
</head>
<body onbeforeunload='return unloadmsg()'>
<div id="editor-container">
<div id="logo">Lurch<span id="check">✓</span></div>
</div>
<script>
unloadmsg = () => { return "Did you save your work?" }
window.addEventListener('load', () => {
// toggle to use the instructor menu
const instructormode = false
// make sure editor.js doesn't show or hide the menu overwriting ours
localStorage.setItem( 'lurch-developer mode on', false )
// options go here
const options = {
preventLeaving: true,
autoSaveEnabled: false,
editor: {
draggable_modal: true,
menubar : 'file edit format math developer help',
font_size_formats: '8pt 9pt 10pt 11pt 12pt 14pt 18pt 24pt 36pt',
content_css : [ 'document',
// `lurchmath/editor-styles.css`,
// `lurchmath/leftborder-theme.css`+`?nocache=${new Date().getTime()}`,
`lurchmath/syntax-theme.css`+`?nocache=${new Date().getTime()}`,
// `lurchmath/syntax-theme.css`,
'https://unpkg.com/[email protected]/dist/mathlive-static.css' ]
},
menuData: {
file: {
title: 'File',
items: 'newlurchdocument opendocument savedocument exportlatex | print'
},
edit: {
title: 'Edit',
items: 'paragraphabove paragraphbelow | undo redo | cut copy paste pastetext | selectall | link unlink openlink | searchreplace | listprops'
},
format: {
title: 'Format',
items: 'expositorymath hr codeformat | styles blocks fontfamily fontsize align lineheight | forecolor backcolor | removeformat'
},
math: {
title: 'Math',
items: 'expression environment | viewdependencyurls togglemeaning validate'
}
},
helpPages: [
{
title: 'Quick Start Guide',
url: 'student.html?load=help/quick-start-guide.lurch'
},
{
title: 'Intro to Proofs in Lurch',
url: 'student.html?load=help/proofs-worksheet.lurch'
},
{
title: 'Example Proofs',
url: 'student.html?load=help/example-proofs.lurch'
},
{
title: 'Lurch Math Reference',
url: 'lde/src/experimental/parsers/lurch-parser-docs.html'
},
{
title: 'Math 299 Course Page',
url: 'https://monks.scranton.edu/math299'
}
],
// fileOpenTabs can be any subset of:
// 'your computer',
// 'the web',
// 'Dropbox',
// 'in-browser storage'
// fileSaveTabs can be any subset of:
// 'your computer',
// 'Dropbox',
// 'in-browser storage'
// fileDeleteTabs can be any subset of:
// 'Dropbox',
// 'in-browser storage'
fileSaveTabs: ['your computer'],
fileOpenTabs: ['your computer', 'the web'],
appRoot: './lurchmath',
appDefaults: {
'notation': 'Lurch notation',
'expression editor type': 'Advanced',
'expository math editor type': 'Advanced',
'dollar sign shortcut': true,
'default shell style': 'minimal',
'application width in window': 'Fixed size',
'developer mode on': false,
'default open dialog tab': 'From your computer',
'default save dialog tab': 'To your computer',
'preferred meaning style': 'Code',
'add LaTeX document wrapper': false,
'export LaTeX selection only': false,
'export LaTeX shells': false
},
documentDefaults: {
'notation': 'Lurch notation',
'shell style': 'minimal'
}
}
// add developer menu if requested
if (instructormode) options.menuData.developer =
{ title: 'Instructor',
items: 'editdependencyurls | extractheader embedheader | redpen | docsettings preferences | downloaddocumentcode'
}
Lurch.createApp(document.getElementById('editor-container'), options)
} )
</script>
</body>
</html>