-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
93 lines (71 loc) · 2.59 KB
/
index.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
<!doctype html>
<title>MMT OnlineTools</title>
<meta charset="utf-8" />
<!-- See index.html for how to fully update CodeMirror versions
In particular, also update the referenced JavaScript file way below.
-->
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.60.0/codemirror.min.css">
<link rel="stylesheet" href="codemirror/theme/dracula.css">
<link rel="stylesheet" href="codemirror/addon/hint/show-hint.css">
<article>
<h1>MMT OnlineTools (<a href="https://github.com/ComFreek/mmteditor">github.com/ComFreek/mmteditor</a>)</h1>
<h2>MMT QuickEditor</h2>
<p>You can also use the <a href="bare.html">full-screen, bare editor</a>.</p>
<form><textarea id="code">namespace http://example.com/mmt-demo ❚
import lfx http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import finite http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
theory Notations =
Pi # { V1T,… } 2 prec -10000❙
lambda # [ V1T,… ] 2 prec -10000❙
apply # 1%w… prec -10❙
arrow # 1⟶… prec -9990❙
case # [ V2T,… ] 1 ⇝ 3 prec 5❙
❚
// Views ❚
view emptyView : ?S -> ?T = ❚
view v : ?S -> ?T =
a = b ❙
c = d ❙
❚</textarea></form>
<p>Type "j" and see autocompletion for Unicode characters appearing!</p>
<h2>How do I type X?</h2>
<p>
Got some line of MMT code with Unicode characters you don't know how to type?<br>
<input type="text" id="typeSearch" size="40" />
</p>
<p>
<ul id="typeResults"></ul>
</p>
<h2>Abbreviation Search (forward & reverse lookup)</h2>
<p>
Enter any (substring) of an abbreviation or Unicode character:<br>
<input type="text" id="abbrSearch" size="20" />
</p>
<p>
<ul id="abbrLookupResults"></ul>
</p>
</article>
<!-- See index.html for how to fully update CodeMirror versions
In particular, also update the referenced CSS file way above.
-->
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.60.0/codemirror.min.js"></script>
<script src="codemirror/addon/hint/show-hint.js"></script>
<script src="codemirror/addon/mode/advanced.js"></script>
<script src="codemirror/mode/mmt/mmt.js"></script>
<script type="module">
import { init as initTypeSearch } from "./typesearch.js";
import { init as initAbbrSearch } from "./abbrsearch.js";
initTypeSearch(
document.getElementById("typeSearch"),
"typeResults"
);
initAbbrSearch(
document.getElementById("abbrSearch"),
document.getElementById("abbrLookupResults")
);
import { init as initEditor } from "./editor.js";
initEditor(document.getElementById("code"));
</script>
</body>
</html>