lean rules

Author: tomaz1502

main.ts

@@ -1,11 +1,10 @@
 import './styles.scss'
-import { MarkdownView, Plugin } from 'obsidian'
+import { Plugin } from 'obsidian'
 
 import './mode/lean/lean'
 
-export default class MLIRSyntaxHighlightPlugin extends Plugin {
+export default class LeanSyntaxHighlightPlugin extends Plugin {
 
-  // these are the CodeMirror modes that Obsidian uses by default
   modesToKeep = ["hypermd", "markdown", "null", "xml"];
 
   onload(): void {
@@ -15,8 +14,6 @@ export default class MLIRSyntaxHighlightPlugin extends Plugin {
   }
 
   onunload() {
-    // Delete all the codemirror modes, to disable the syntax highlighting
-    // except the default ones, obviously
     for (const key in CodeMirror.modes) {
       if (CodeMirror.modes.hasOwnProperty(key) && !this.modesToKeep.includes(key)) {
         delete CodeMirror.modes[key];
@@ -27,7 +24,6 @@ export default class MLIRSyntaxHighlightPlugin extends Plugin {
   }
 
   refreshLeaves = () => {
-    // re-set the editor mode to refresh the syntax highlighting
     this.app.workspace.iterateCodeMirrors(cm => cm.setOption("mode", cm.getOption("mode")))
   }
 }

mode/lean/lean.js

@@ -6,5 +6,21 @@
   else
     mod(CodeMirror)
 })(function(CodeMirror) {
-    // TODO
+  "use strict"
+  CodeMirror.defineSimpleMode("lean", {
+    start: [
+      { regex: /\b0b[01]+\b/i, token: "number" },
+      { regex: /\b0o[0-7]+\b/i, token: "number" },
+      { regex: /\b0x[0-9a-f]+\b/i, token: "number" },
+      { regex: /\b-?\d+(?:\.\d+)?(?:e[-+]?\d+)?\b/i, token: "number" },
+      { regex: /(?:\/-[\s\S]*?-\/)|(?:--.*$)/m, token: "comment" },
+      { regex: /\b(?:theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break|global|local|scoped|partial|unsafe|private|protected|noncomputable)\b/, token: "keyword" },
+      { regex: /#(print|check|eval|reduce|check_failure)/, token: "operator" },
+      { regex: /\+|\*|-|\/|:=|>>>|<<<|\^\^\^|&&&|\|\|\||\+\+|\^|%|~~~|<|<=|>|>=|==|=/, token: "operator" },
+      { regex: /[()\[\]{},:]/, token: "meta" },
+      { regex: /\b(?:true|false)\b/, token: "attribute" },
+      { regex: /\b(?:sorry|admit)\b/, token: "operator" },
+      // { regex: /(\b(?:inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant))(\s+)(\w+)/, token: ["keyword", null, "function"] }
+    ]
+  })
 });