KDE Syntax Highlighting XML file for Lean

lean.xml

<?xml version="1.0" encoding="UTF-8"?>
<!--
  based on pygments highlighting file for Lean4 (https://github.com/leanprover/lean4/blob/master/doc/latex/lean4.py)
  and VSCode highlighting file for Lean4 (https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json).
-->
<language name="Lean" version="1" kateversion="2.4" section="Sources" extensions="*.lean;*.lean4"
    mimetype="text/x-lean">

    <highlighting>

        <!-- {
        "name": "Lean 4",
        "scopeName": "source.lean4",
        "fileTypes": [],
        "patterns": [-->

        <!-- TODO { "include": "#comments" }, -->
        <!-- { "match": "\\b(Prop|Type|Sort)\\b", "name": "storage.type.lean4" }, -->
        <list name="Types"> <!-- dsBuiltIn -->
            <item>Prop</item>
            <item>Type</item>
            <item>Sort</item>
        </list>
        <!-- { "match": "\\battribute\\b\\s*\\[[^\\]]*\\]", "name": "storage.modifier.lean4" }, -->
        <list name="attribute"> <!-- dsAttribute -->
            <item>attribute</item>
        </list>

        <!-- { "match": "@\\[[^\\]]*\\]", "name": "storage.modifier.lean4" },-->
        <!--{
            "match":
        "\\b(?<!\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\.)\\b",
            "name": "storage.modifier.lean4"
          }, -->
        <list name="Modifiers"> <!-- dsAttribute -->
            <item>global</item>
            <item>local</item>
            <item>scoped</item>
            <item>partial</item>
            <item>unsafe</item>
            <item>private</item>
            <item>protected</item>
            <item>noncomputable</item>
        </list>
        <!-- { "match": "\\bsorry\\b", "name": "invalid.illegal.lean4" }, -->
        <list name="sorry"> <!-- dsWarning -->
            <item>sorry</item>
            <item>admit</item>
        </list>
        <!-- { "match": "#(print|eval|reduce|check|check_failure)\\b", "name": "keyword.other.lean4"
        }, -->
        <list name="Commands"> <!-- dsPreprocessor -->
            <item>#print</item>
            <item>#eval</item>
            <item>#reduce</item>
            <item>#check</item>
            <item>#check_failure</item>
            <item>#align</item>
        </list>
        <!-- TODO {
            "match": "\\bderiving\\s+instance\\b",
            "name": "keyword.other.command.lean4"
          }, -->
        <!-- {
            "begin":
        "\\b(?<!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?",
            "beginCaptures": {
              "1": {"name": "keyword.other.definitioncommand.lean4"}
            },
            "patterns": [
              {"include": "#comments"},
              {"include": "#definitionName"},
              {"match": ","}
            ],
            "end": "(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[:\\|\\(\\[\\{⦃<>])",
            "name": "meta.definitioncommand.lean4"
          }, -->
        <list name="Definitions"> <!-- dsKeyword --> <!-- dsFunction until with -->
            <item>inductive</item>
            <item>coinductive</item>
            <item>structure</item>
            <item>theorem</item>
            <item>axiom</item>
            <item>abbrev</item>
            <item>lemma</item>
            <item>def</item>
            <item>instance</item>
            <item>class</item>
            <item>constant</item>
        </list>
        <list name="DefinitionsAfterName">
            <item>with</item>
            <item>extends</item>
            <item>where</item>
            <!-- <item>:</item>
            <item>|</item>
            <item>(</item>
            <item>[</item>
            <item>{</item>
            <item>⦃</item>
            <item><</item>
            <item>></item> -->
        </list>
        <!-- {
            "match":
        "\\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)(?!\\.)\\b",
            "name": "keyword.other.lean4"
          }, -->
        <list name="import"> <!-- dsImport -->
            <item>import</item>
        </list>
        <list name="ControlFlows"> <!-- dsControlFlow -->
            <item>if</item>
            <item>then</item>
            <item>else</item>
            <item>calc</item>
            <item>match</item>
            <item>try</item>
            <item>catch</item>
            <item>finally</item>
            <item>return</item>
            <item>continue</item>
            <item>break</item>
            <item>for</item>
            <item>do</item>
        </list>
        <list name="Keywords"> <!-- dsKeyword -->
            <item>theorem</item>
            <item>def</item>
            <item>class</item>
            <item>axiom</item>
            <item>constant</item>
            <item>universe</item>
            <item>universes</item>
            <item>variable</item>
            <item>variables</item>
            <item>example</item>
            <item>structure</item>
            <item>instance</item>
            <item>postfix</item>
            <item>prefix</item>
            <item>notation</item>
            <item>abbrev</item>
            <item>infix</item>
            <item>infixl</item>
            <item>infixr</item>
            <item>show</item>
            <item>have</item>
            <item>from</item>
            <item>suffices</item>
            <item>nomatch</item>
            <item>set_option</item>
            <item>initialize</item>
            <item>builtin_initialize</item>
            <item>inductive</item>
            <item>coinductive</item>
            <item>open</item>
            <item>export</item>
            <item>theory</item>
            <item>prelude</item>
            <item>renaming</item>
            <item>hiding</item>
            <item>exposing</item>
            <item>by</item>
            <item>let</item>
            <item>extends</item>
            <item>mutual</item>
            <item>mut</item>
            <item>where</item>
            <item>rec</item>
            <item>syntax</item>
            <item>macro_rules</item>
            <item>macro</item>
            <item>deriving</item>
            <item>fun</item>
            <item>section</item>
            <item>namespace</item>
            <item>end</item>
            <item>with</item>
            <item>in</item>
            <item>unless</item>
            <item>at</item>
            <item>use</item>
            <item>begin</item>
        </list>
        <list name="Tactics">
            <item>intro</item>
            <item>intros</item>
            <item>rename</item>
            <item>revert</item>
            <item>clear</item>
            <item>subst</item>
            <item>subst_vars</item>
            <item>assumption</item>
            <item>contradiction</item>
            <item>apply</item>
            <item>exact</item>
            <item>refine</item>
            <item>refine'</item>
            <item>constructor</item>
            <item>case</item>
            <item>case'</item>
            <item>all_goals</item>
            <item>any_goals</item>
            <item>trace</item>
            <item>first</item>
            <item>rotate_left</item>
            <item>rotate_right</item>
            <item>try</item>
            <item>rfl</item>
            <item>rfl'</item>
            <item>ac_rfl</item>
            <item>sorry</item>
            <item>admit</item>
            <item>infer_instance</item>
            <item>change</item>
            <item>rewrite</item>
            <item>rw</item>
            <item>injection</item>
            <item>injections</item>
            <item>simp</item>
            <item>simp_all</item>
            <item>dsimp</item>
            <item>delta</item>
            <item>unfold</item>
            <item>refine_lift</item>
            <item>have</item>
            <item>suffices</item>
            <item>let</item>
            <item>show</item>
            <item>refine_lift'</item>
            <item>have'</item>
            <item>let'</item>
            <item>induction</item>
            <item>generalize</item>
            <item>cases</item>
            <item>rename_i</item>
            <item>repeat</item>
            <item>trivial</item>
            <item>split</item>
            <item>stop</item>
            <item>specialize</item>
            <item>unhygienic</item>
            <item>fail</item>
            <item>checkpoint</item>
            <item>save</item>
            <item>sleep</item>
            <item>exists</item>
            <item>congr</item>
            <item>simp</item>

            <item>introv</item>
            <item>transitivity</item>
            <item>use</item>
            <item>inductive'</item>
            <item>rcases</item>
            <item>obtain</item>
            <item>by_cases</item>
            <item>simpa</item>
            <item>cases'</item>
            <item>contrapose!</item>
            <item>contrapose</item>
            <item>rwa</item>
            <item>ext</item>
            <item>push_neg</item>
            <item>nth_rw</item>
            <item>by_contra</item>
            <item>by_contra'</item>
            <item>conv_rhs</item>
            <item>conv_lhs</item>
            <item>linarith</item>
            <item>library_search</item>
            <item>rintro</item>
            <item>rintros</item>
            <item>choose</item>
            <item>ring</item>
            <item>exfalso</item>
            <item>by_contradiction</item>
            <item>by_contradiction'</item>
            <item>left</item>
            <item>right</item>
            <item>refl</item>

            <item>from</item>
            <item>using</item>
        </list>
        <!-- { "begin": "«", "end": "»", "contentName": "entity.name.lean4" }, -->
        <!-- {
            "begin": "\"", "end": "\"",
            "name": "string.quoted.double.lean4",
            "patterns": [
              { "match": "\\\\[\\\\\"ntr']", "name": "constant.character.escape.lean4" },
              { "match": "\\\\x[0-9A-Fa-f][0-9A-Fa-f]", "name": "constant.character.escape.lean4" },
              { "match": "\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]", "name":
        "constant.character.escape.lean4" }
            ]
          }, -->
        <!-- { "name": "constant.language.lean4", "match": "\\b(true|false)\\b" }, -->
        <list name="Constants"> <!-- dsConstant -->
            <item>true</item>
            <item>false</item>
        </list>
        <!-- TODO { "name": "string.quoted.single.lean4", "match": "'[^\\\\']'" },
          { "name": "string.quoted.single.lean4", "match":
        "'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'",
            "captures": { "1": { "name": "constant.character.escape.lean4" } } },
          { "match": "`+[^\\[(]\\S+", "name": "entity.name.lean4" },-->
        <!-- { "match":
        "\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\b",
        "name": "constant.numeric.lean4" } -->
        <!-- ], -->
        <!--"repository":
        {
          "definitionName": {
            "patterns": [
              {"match": "\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*", "name":
        "entity.name.function.lean4"},
              {"begin": "«", "end": "»", "contentName": "entity.name.function.lean4"}
            ]
          },
          "dashComment": {
            "begin": "--><!--", "end": "$",
            "name": "comment.line.double-dash.lean4",
            "patterns": [
              { "include": "source.lean.markdown" }
            ]
          },
          "docComment": {
            "begin": "/--><!--", "end": "-/", "name": "comment.block.documentation.lean4",
            "patterns": [
              { "include": "source.lean.markdown" },
              { "include": "#blockComment" }
            ]
          },
          "modDocComment": {
            "begin": "/-!", "end": "-/", "name": "comment.block.documentation.lean4",
            "patterns": [
              { "include": "source.lean.markdown" },
              { "include": "#blockComment" }
            ]
          },
          "blockComment": {
            "begin": "/-", "end": "-/", "name": "comment.block.lean4",
            "patterns": [
              { "include": "source.lean.markdown" },
              { "include": "#blockComment" }
            ]
          },
          "comments": {
            "patterns": [
              { "include": "#dashComment" },
              { "include": "#docComment" },
              { "include": "#stringBlock" },
              { "include": "#modDocComment" },
              { "include": "#blockComment" }
            ]
          }
        }
        } -->


        <contexts>
            <context attribute="Normal Text" lineEndContext="#stay" name="Normal Text">
                <keyword attribute="Types" context="#stay" String="Types" />
                <keyword attribute="Modifiers" context="#stay" String="Modifiers" />
                <RegExpr attribute="Modifiers" context="#stay" String="(?:attribute\b\s*|@)\[[^\]]*\]" />
                <keyword attribute="sorry" context="#stay" String="sorry" />
                <keyword attribute="Commands" context="#stay" String="Commands" />
                <keyword attribute="import" context="Importing" String="import" />
                <keyword attribute="ControlFlows" context="#stay" String="ControlFlows" />
                <keyword attribute="Definitions" context="defining" String="Definitions" />
                <keyword attribute="Tactics" context="#stay" String="Tactics" />
                <keyword attribute="Keywords" context="#stay" String="Keywords" />
                <keyword attribute="Constants" context="#stay" String="Constants" />

                <RangeDetect attribute="NameEscape" context="#stay" char="«" char1="»" />
                <RegExpr attribute="Name" context="#stay"
                    String="[A-Za-z_&#x03b1;-&#x03ba;&#x03bc;-&#x03fb;&#x1f00;-&#x1ffe;&#x2100;-&#x214f;][A-Za-z_'&#x03b1;-&#x03ba;&#x03bc;-&#x03fb;&#x1f00;-&#x1ffe;&#x2070;-&#x2079;&#x207f;-&#x2089;&#x2090;-&#x209c;&#x2100;-&#x214f;0-9]*" />
                <RegExpr attribute="Hexadecimal" context="#stay" String="0[xX][0-9a-fA-F]+" />
                <RegExpr attribute="Float" context="#stay" String="[0-9]+(?:(\.[0-9]*)?[eE][+-]?[0-9]+|\.[0-9]*)" />
                <RegExpr attribute="Decimal" context="#stay" String="[0-9]+" />
                <DetectChar attribute="String" context="string" char="&quot;" />
                <StringDetect attribute="Comment" context="#stay" String="/--/" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
                <StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
                <StringDetect lookAhead="true" context="SingleLineComment" String="--" />


                <!-- <StringDetect attribute="Operation" context="#stay" String="..." />
                <StringDetect attribute="Operation" context="#stay" String="<;>" />
                <StringDetect attribute="Operation" context="#stay" String="|-" />
                <StringDetect attribute="Operation" context="#stay" String=":=" />
                <StringDetect attribute="Operation" context="#stay" String="!=" />
                <StringDetect attribute="Operation" context="#stay" String="#&amp;" />
                <StringDetect attribute="Operation" context="#stay" String="-." />
                <StringDetect attribute="Operation" context="#stay" String="->" />
                <StringDetect attribute="Operation" context="#stay" String=".." />
                <StringDetect attribute="Operation" context="#stay" String="::" />
                <StringDetect attribute="Operation" context="#stay" String=":>" />
                <StringDetect attribute="Operation" context="#stay" String=";;" />
                <StringDetect attribute="Operation" context="#stay" String="&lt;-" />
                <StringDetect attribute="Operation" context="#stay" String="==" />
                <StringDetect attribute="Operation" context="#stay" String="||" />
                <StringDetect attribute="Operation" context="#stay" String="&lt;-" />
                <StringDetect attribute="Operation" context="#stay" String="=>" />
                <StringDetect attribute="Operation" context="#stay" String="&lt;=" />
                <StringDetect attribute="Operation" context="#stay" String=">=" />
                <StringDetect attribute="Operation" context="#stay" String="/\" />
                <StringDetect attribute="Operation" context="#stay" String="\/" />
                <StringDetect attribute="Operation" context="#stay" String="⁻¹" />
                <AnyChar attribute="Operation" context="#stay"
                String="#&amp;*+-/@!`.;&lt;=>_|~∀Πλ↔∧∨≠≤≥¬⬝▸←→∃≈×⌞⌟≡⟨⟩⊢‹›" />
                <AnyChar attribute="Constants" context="#stay" String="ℕℤ" /> -->
            </context>

            <context attribute="Comment" lineEndContext="#pop" name="SingleLineComment">
            </context>

            <context attribute="Comment" lineEndContext="#stay" name="MultiLineComment">
                <StringDetect attribute="Comment" context="#pop" String="-/" />
                <StringDetect attribute="Comment" context="#stay" String="/--/" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
                <StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
            </context>

            <context attribute="DocComment" lineEndContext="#stay" name="DocMultiLineComment">
                <StringDetect attribute="DocComment" context="#pop" String="-/" />
                <StringDetect attribute="Comment" context="#stay" String="/--/" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/-!" />
                <StringDetect attribute="DocComment" context="DocMultiLineComment" String="/--" />
                <StringDetect attribute="Comment" context="MultiLineComment" String="/-" />
            </context>

            <context attribute="String" lineEndContext="#stay" name="string">
                <DetectChar attribute="String" context="#pop" char="&quot;" />
                <RegExpr attribute="StringEscape" context="#stay"
                    String="\\(?:[\\&quot;ntr']|x[0-9A-Fa-f]{2}|u[0-9A-Fa-f]{4})" />
                <DetectChar attribute="ErrorStringEscape" context="#stay" char="\" />
            </context>

            <context attribute="Importing" lineEndContext="#pop" name="Importing">
            </context>

            <context attribute="Defining" lineEndContext="#stay" name="defining">
                <keyword attribute="DefinitionsAfterName" context="#pop"
                    String="DefinitionsAfterName" />
                <AnyChar attribute="String" context="#pop" String="&quot;:|([{⦃&lt;>"
                    lookAhead="true" />
            </context>
        </contexts>

        <itemDatas>
            <itemData name="Normal Text" defStyleNum="dsNormal" spellChecking="false" />
            <itemData name="Types" defStyleNum="dsBuiltIn" spellChecking="false" />
            <itemData name="Modifiers" defStyleNum="dsAttribute" spellChecking="false" />
            <itemData name="sorry" defStyleNum="dsWarning" spellChecking="false" />
            <itemData name="Commands" defStyleNum="dsPreprocessor" spellChecking="false" />
            <itemData name="import" defStyleNum="dsKeyword" spellChecking="false" />
            <itemData name="ControlFlows" defStyleNum="dsControlFlow" spellChecking="false" />
            <itemData name="Definitions" defStyleNum="dsKeyword" spellChecking="false" />
            <itemData name="DefinitionsAfterName" defStyleNum="dsKeyword" spellChecking="false" />

            <!-- <itemData name="Operation" defStyleNum="dsOperator" spellChecking="false"/> -->

            <itemData name="Tactics" defStyleNum="dsKeyword" spellChecking="false" />
            <itemData name="Keywords" defStyleNum="dsKeyword" spellChecking="false" />
            <itemData name="Constants" defStyleNum="dsConstant" spellChecking="false" />

            <itemData name="NameEscape" defStyleNum="dsNormal" spellChecking="false" />
            <itemData name="Name" defStyleNum="dsNormal" spellChecking="false" />
            <itemData name="Hexadecimal" defStyleNum="dsBaseN" spellChecking="false" />
            <itemData name="Float" defStyleNum="dsFloat" spellChecking="false" />
            <itemData name="Decimal" defStyleNum="dsDecVal" spellChecking="false" />

            <itemData name="Defining" defStyleNum="dsFunction" spellChecking="false" />
            <itemData name="Importing" defStyleNum="dsImport" spellChecking="false" />
            <itemData name="String" defStyleNum="dsString" spellChecking="false" />
            <itemData name="StringEscape" defStyleNum="dsSpecialChar" spellChecking="false" />
            <itemData name="ErrorStringEscape" defStyleNum="dsError" spellChecking="false" />
            <itemData name="Comment" defStyleNum="dsComment" />
            <itemData name="DocComment" defStyleNum="dsDocumentation" />
        </itemDatas>
    </highlighting>
    <general>
        <comments>
            <comment name="singleLine" start="--" position="afterwhitespace" />
            <comment name="multiLine" start="/-" end="-/" />
        </comments>
        <keywords casesensitive="1" weakDeliminator="#._"
            additionalDeliminator="#&amp;*+-/!`;&lt;=>_|~∀Πλ↔∧∨≠≤≥¬·⬝▸←→∃≈×⌞⌟≡⟨⟩⊢‹›⦃⦄" />
        <folding indentationsensitive="1" />
    </general>
</language>