-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathscratchpad.html
63 lines (52 loc) · 2.17 KB
/
scratchpad.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
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<link rel="icon" href="ui-images/favicon.png">
<title>jsCoq – The Coq Theorem Prover Online IDE</title>
<style>
/* Allow some extra scroll space at the bottom & to the right */
.CodeMirror-lines {
padding-bottom: 75% !important;
padding-right: 40px !important;
}
</style>
</head>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled" data-filename="scratchpad.v">
<!-- Editor and panel are created here by CoqManager -->
</div>
<script type="module">
import { JsCoq } from "./node_modules/jscoq/jscoq.js";
var sp = new URLSearchParams(location.search),
panel_theme = sp.has('dark') ? 'dark' : sp.get('theme') || 'light',
editor_theme = sp.get('editor_theme') || (panel_theme == 'dark' ? 'blackboard' : 'default');
var jscoq_opts = {
backend: sp.get('backend'),
subproc: sp.has('app'),
file_dialog: true,
implicit_libs: true,
editor: { mode: { 'company-coq': true }, theme: editor_theme },
theme: panel_theme
};
/* Global reference */
var coq, last_filename = localStorage['scratchpad.last_filename'],
set_filename = fn => document.getElementById('ide-wrapper')
.setAttribute('data-filename', fn);
if (sp.has('code')) set_filename('');
else if (last_filename) set_filename(last_filename);
JsCoq.start(jscoq_opts).then(res => {
coq = res;
if (sp.has('project')) coq.openProject(sp.get('project'));
if (sp.has('share')) coq.openCollab({hastebin: sp.get('share')});
if (sp.has('p2p')) coq.openCollab({p2p: sp.get('p2p')});
if (sp.has('code')) coq.provider.load(sp.get('code'), sp.get('fn') || 'playground');
});
window.addEventListener('beforeunload', () => {
var sp = coq.provider.snippets[0];
localStorage['scratchpad.last_filename'] = sp.filename;
});
</script>
</body>
</html>