-
Notifications
You must be signed in to change notification settings - Fork 9
/
index.html
86 lines (86 loc) · 3.54 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
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8" />
<title>TopShell</title>
<meta name="description" content="Purely functional terminal and shell" />
<link href="https://maxcdn.bootstrapcdn.com/font-awesome/4.7.0/css/font-awesome.min.css" rel="stylesheet" />
<link href="https://fonts.googleapis.com/css?family=Montserrat|Fira+Mono" rel="stylesheet" />
<script crossorigin src="https://unpkg.com/react@16/umd/react.production.min.js"></script>
<script crossorigin src="https://unpkg.com/react-dom@16/umd/react-dom.production.min.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/codemirror.js"></script>
<link href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/codemirror.css" rel="stylesheet" />
<!--script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/dialog/dialog.js"></script>
<link href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/dialog/dialog.css" rel="stylesheet" />
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/search/searchcursor.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/search/search.js"></script-->
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/hint/show-hint.js"></script>
<link href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.0/addon/hint/show-hint.css" rel="stylesheet" />
<script src="target/scala-2.12/topshell-opt.js"></script>
<script src="../modules.js"></script>
<script src="editor.js"></script>
<style>
.CodeMirror {
width: 100%;
height: 100%;
font-family: 'Fira Mono', monospace;
font-size: 14px;
color: #d716d4;
}
.CodeMirror-lines {
padding-top: 10px;
padding-bottom: 10px;
}
.CodeMirror-gutters {
background-color: #ffffff;
border: none;
}
.CodeMirror-hints {
font-family: 'Fira Mono', monospace;
font-size: 14px;
border-radius: 0;
border: none;
box-shadow: 0 1px 2px 1px rgba(150, 150, 150, 0.6);
background-color: #ffffff;
line-height: 25px;
}
.editor-gutter {
width: 15px;
}
.topshell-hint-module {
color: #268d3d;
}
.topshell-hint-type {
color: #909090;
}
li.CodeMirror-hint-active {
background-color: #e0f0f0;
color: #000000;
}
.CodeMirror .cm-keyword {
color: #268d3d;
}
.CodeMirror .cm-attribute {
color: #000000;
}
.CodeMirror .cm-variable {
color: #265ccc;
}
.CodeMirror .cm-operator {
color: #d716d4;
}
.CodeMirror .cm-string {
color: #c00000;
}
.CodeMirror .cm-number {
color: #c00000;
}
.CodeMirror .cm-comment {
color: #909090;
}
</style>
</head>
<body style="padding: 0; margin: 0; background-color: #ffffff; overflow: hidden">
<div id="main"></div>
</body>
</html>