diff options
Diffstat (limited to 'ide/highlight.mll')
| -rw-r--r-- | ide/highlight.mll | 86 |
1 files changed, 65 insertions, 21 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll index e2a1d0cd..27ead696 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll,v 1.14.2.2 2004/11/27 14:41:43 herbelin Exp $ *) +(* $Id: highlight.mll 8880 2006-05-31 10:52:08Z notin $ *) { @@ -18,6 +18,39 @@ let comment_start = ref 0 + let is_keyword = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Add" ; "Check"; "Defined" ; + "End" ; "Eval"; "Export" ; "Extraction" ; "Hint" ; "Hints" ; + "Implicits" ; "Import" ; + "Infix" ; "Load" ; "Module" ; + "Notation"; "Proof" ; "Print"; "Qed" ; + "Require" ; "Reset"; "Undo"; "Save" ; + "Section" ; "Unset" ; + "Set" ; "Notation" + ]; + Hashtbl.mem h + + let is_constr_kw = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; + "end"; "as"; "let"; "if"; "then"; "else"; "return"; + "Prop"; "Set"; "Type"]; + Hashtbl.mem h + + let is_declaration = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ; + "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; + "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; + "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; + "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters" + ]; + Hashtbl.mem h + } let space = @@ -28,30 +61,41 @@ let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let ident = firstchar identchar* -let keyword = - "Add" | "Defined" | - "End" | "Export" | "Extraction" | "Hint" | - "Implicits" | "Import" | - "Infix" | "Load" | "match" | "Module" | "Module Type" | - "Proof" | "Qed" | - "Require" | "Save" | "Scheme" | - "Section" | "Unset" | - "Set" +let thm_token = "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" + +let def_token = "Definition" | "Let" | "Example" | "SubClass" + +let assumption = "Hypothesis" | "Variable" | "Axiom" | "Parameter" | "Conjecture" | + "Hypotheses" | "Variables" | "Axioms" | "Parameters" let declaration = - "Lemma" | "Axiom" | "CoFixpoint" | "Definition" | - "Fixpoint" | "Hypothesis" | - "Hypotheses" | "Axioms" | "Parameters" | "Subclass" | - "Remark" | "Fact" | "Conjecture" | "Let" | - "CoInductive" | "Record" | "Structure" | - "Inductive" | "Parameter" | "Theorem" | - "Variable" | "Variables" + "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" | + "Definition" | "Let" | "Example" | "SubClass" | + "Inductive" | "CoInductive" | + "Record" | "Structure" | + "Fixpoint" | "CoFixpoint" rule next_order = parse - | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } - | keyword { lexeme_start lexbuf,lexeme_end lexbuf, "kwd" } - | declaration space+ ident (space* ',' space* ident)* - { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } + | "(*" + { comment_start := lexeme_start lexbuf; comment lexbuf } + | "Module Type" + { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } + | ident as id + { if is_keyword id then + lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + else + begin + if is_constr_kw id then + lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + else + begin + if is_declaration id then + lexeme_start lexbuf, lexeme_end lexbuf, "decl" + else + next_order lexbuf + end + end + } | _ { next_order lexbuf} | eof { raise End_of_file } |