diff options
Diffstat (limited to 'ide/highlight.mll')
-rw-r--r-- | ide/highlight.mll | 26 |
1 files changed, 9 insertions, 17 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll index 9c0e5abee..4bc200ada 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -29,27 +29,19 @@ let identchar = let ident = firstchar identchar* let keyword = - "Add" | "AddPath" | "Chapter" | "Check" | - "CoInductive" | "Compile" | "Defined" | - "End" | "Export" | "Extraction" | "Fact" | "Fix" | "Global" | - "Grammar" | "Hint" | - "Hints" | ("Hints" space+ "Resolve") | - "Immediate" | "Implicits" | "Import" | - "Infix" | "Load" | "LoadPath" | "Local" | - "Match" | "Module" | "Module Type" | - "Mutual" | "Print" | "Proof" | "Qed" | - "Record" | "Recursive" | - ("Require" (space+ "Export")? space+ ident) | "Save" | "Scheme" | - "Section" | "Show" | "Syntactic" | "Syntax" | "Tactic" | - "Unset" | - ("Set" space+ "Implicit" space+ "Arguments") | - ("Implicit" space+ "Arguments" space+ ("On" | "Off")) | "Cases" + "Add" | "CoInductive" | "Defined" | + "End" | "Export" | "Extraction" | "Hint" | + "Implicits" | "Import" | + "Infix" | "Load" | "match" | "Module" | "Module Type" | + "Proof" | "Qed" | + "Record" | "Require" | "Save" | "Scheme" | + "Section" | "Unset" | + "Set" let declaration = "Lemma" | "Axiom" | "CoFixpoint" | "Definition" | - ("Tactic" space+ "Definition") | "Fixpoint" | "Hypothesis" | - "Inductive" | "Parameter" | "Remark" | "Theorem" | + "Inductive" | "Parameter" | "Theorem" | "Variable" | "Variables" rule next_order = parse |