<commit_before>import * as CodeMirror from "codemirror";

/*
This is just a first tiny quick step.  To finish this:

- Look at https://codemirror.net/demo/simplemode.html for how this works.
- Put everything from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json in here.

NOTE(hsy): I think the alternative that works with safari is this negative look ahead

/((?!\.).{1}|^)\b(import|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd)\b/gm

playgroud: https://regex101.com/r/lop9Se/1

*/

(CodeMirror as any).defineSimpleMode("lean", {
  start: [
    { regex: /"(?:[^\\]|\\.)*?(?:"|$)/, token: "string" },
    {
      regex: /#(print|eval|reduce|check|help|exit)\b/,
      token: "keyword"
    },
    {
      regex: /\b(?!\.)(import|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd)\b/,
      token: "keyword"
    },
    {
      regex: /\b(?!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from)\b/,
      token: "keyword"
    },
    {
      regex: /\b(Prop|Type|Sort)\b/,
      token: "keyword"
    },
    {
      regex: /0x[a-f\d]+|[-+]?(?:\.\d+|\d+\.?\d*)(?:e[-+]?\d+)?/i,
      token: "number"
    },
    { regex: /--.*/, token: "comment" },
    { regex: /[-+\/*=<>!]+/, token: "operator" },
    { regex: /begin/, indent: true },
    { regex: /end/, dedent: true },
    { regex: /[a-z$][\w$]*/, token: "variable" }
  ],
  string: [
    { regex: /"/, token: "string", next: "start" },
    { regex: /(?:[^\\"]|\\(?:.|$))*/, token: "string" }
  ],
  comment: [{ regex: /\(-.*-\)/, token: "comment", next: "start" }],
  meta: {
    dontIndentStates: ["comment"],
    /* electricInput: /^\s*\}$/, */
    blockCommentStart: "(-",
    blockCommentEnd: "-)",
    lineComment: "--"
  }
});<commit_msg>webapp/lean syntax: support block comments, rearrangements, etc.<commit_after>import * as CodeMirror from "codemirror";

/*
This is just a first tiny quick step.  To finish this:

- Look at https://codemirror.net/demo/simplemode.html for how this works.
- Put everything from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json in here.

playgroud to see the alternative of negative look ahead in action: https://regex101.com/r/lop9Se/1

*/

(CodeMirror as any).defineSimpleMode("lean", {
  start: [
    { regex: /"(?:[^\\]|\\.)*?(?:"|$)/, token: "string" },
    { regex: /\/-/, token: "comment", next: "blockcomment" },
    {
      regex: /#(print|eval|reduce|check|help|exit)\b/,
      token: "variable-3"
    },
    { regex: /--.*/, token: "comment" },
    { regex: /[-+\/*=<>!]+/, token: "operator" },
    {
      regex: /((?!\.).{1}|^)\b(import|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd)\b/,
      token: "keyword"
    },
    {
      regex: /((?!\.).{1}|^)\b(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from)\b/,
      token: "variable-2"
    },
    {
      regex: /\b(Prop|Type|Sort)\b/,
      token: "atom"
    },
    {
      regex: /0x[a-f\d]+|[-+]?(?:\.\d+|\d+\.?\d*)(?:e[-+]?\d+)?/i,
      token: "number"
    },
    { regex: /\/-.*?-\//, token: "comment" },
    { regex: /begin/, indent: true },
    { regex: /end/, dedent: true },
    { regex: /[a-z$][\w$]*/, token: "variable" },
    { regex: /b?"/, token: "string", next: "string" }
  ],
  string: [
    { regex: /"/, token: "string", next: "start" },
    { regex: /(?:[^\\"]|\\(?:.|$))*/, token: "string" }
  ],
  blockcomment: [
    { regex: /.*?-\//, token: "comment", next: "start" },
    { regex: /.*/, token: "comment" }
  ],
  meta: {
    dontIndentStates: ["comment"],
    lineComment: "--"
  }
});
{'fraction_non_alphanumeric': 0.22823275862068965, 'fraction_numerical': 0.003663793103448276, 'mean_word_length': 3.8193146417445485, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 6, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2257463', 'n_tokens_mistral': 1751, 'n_tokens_neox': 1718, 'n_words': 242}