Temporary webppl keyword style (bold)

probmods · Sep 22, 2016 · b3e64d7 · b3e64d7
1 parent 52ee56d
commit b3e64d7
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/src/component.css b/src/component.css
@@ -33,6 +33,13 @@
     color: black;
     background-color: #ECAAB9;
 }
+
+/* wppl keywords */
+
+.cm-wppl {
+    font-weight: bold
+}
+
 /* -- folding */
 .wpedit .CodeMirror-foldmarker {
     background-color: #ffffcc;

diff --git a/src/index.js b/src/index.js
@@ -11,7 +11,8 @@ var CodeMirrorComponent = require('react-codemirror');
 var Folding = require('./folding')(CodeMirror);
 require('codemirror/addon/edit/matchbrackets');
 require('codemirror/addon/edit/closebrackets');
-require('codemirror/mode/javascript/javascript');
+//require('codemirror/mode/javascript/javascript');
+require('./wppl-mode.js')
 require('codemirror/addon/comment/comment'); // installs toggleComment
 
 var wait = function(ms, f) {