File tree Expand file tree Collapse file tree 6 files changed +7
-10395
lines changed Expand file tree Collapse file tree 6 files changed +7
-10395
lines changed Original file line number Diff line number Diff line change 4
4
< meta charset ="utf-8 "/>
5
5
< link rel =stylesheet href ="src/docs.css ">
6
6
7
- < link rel ="stylesheet " href ="src/codemirror.css ">
8
- < link rel ="stylesheet " href ="src/3024-night.css ">
9
- < script src ="src/codemirror.js "> </ script >
10
- < script src ="src/matchbrackets.js "> </ script >
11
- < script src ="../lambdacalc.js "> </ script >
7
+ < link rel ="stylesheet " href ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.65.1/codemirror.min.css ">
8
+ < link rel ="stylesheet " href ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.65.1/theme/3024-night.min.css ">
9
+ < link rel ="stylesheet " href ="https://fonts.googleapis.com/css?family=Source+Sans+Pro ">
10
+
12
11
< style > .CodeMirror {border-top : 1px solid black; border-bottom : 1px solid black;}</ style >
13
12
< div id =nav >
14
13
< a href ="https://codemirror.net "> < h1 > CodeMirror</ h1 > < img id =logo src ="../../doc/logo.png " alt =""> </ a >
@@ -78,6 +77,9 @@ <h2>Lambda Calculus mode</h2>
78
77
allf = \ f xs . all (map f xs)
79
78
</ textarea > </ form >
80
79
80
+ < script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.65.1/codemirror.min.js "> </ script >
81
+ < script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.65.1/addon/edit/matchbrackets.min.js "> </ script >
82
+ < script src ="../lambdacalc.js "> </ script >
81
83
< script >
82
84
var editor = CodeMirror . fromTextArea ( document . getElementById ( "code" ) , {
83
85
lineNumbers : true ,
Load Diff This file was deleted.
You can’t perform that action at this time.
0 commit comments