IDE:coloration

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3726 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 36 deletions

diff --git a/ide/highlight.mll b/ide/highlight.mll
index 5e624fdf26..76a845f6e8 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -8,54 +8,36 @@
 
   let comment_start = ref 0
 
-  let kwd = [
-  "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
-  "CoInductive";  "Compile"; "Defined"; "Definition"; 
-  "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
-  "Hints"; "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
-  "Infix"; "Lemma"; "Load"; "Local"; 
-  "Match"; "Module"; "Module Type";
-  "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
-  "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-  "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-  "Unset"; "Variable"; "Variables"; 
-  ]
-
-module SHashtbl = 
-  Hashtbl.Make 
-    (struct 
-       type t = string
-       let equal = ( = )
-       let hash = Hashtbl.hash
-     end)
-
-let word_tbl = SHashtbl.create 37
-let _ =  List.iter (fun w -> SHashtbl.add word_tbl w "kwd") kwd
 }
 
+let space = 
+  [' ' '\010' '\013' '\009' '\012']
+let firstchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let ident = firstchar identchar*
+
 let keyword = 
   "Add" | "AddPath" | "Chapter" |
   "CoInductive" |  "Compile" | "Defined" | 
   "End" | "Export" | "Fact" | "Fix" | "Global" | 
   "Grammar" | "Hint" |
-  "Hints" | "Immediate" | "Implicits" | "Import" | 
-  "Infix" | "Load" | "Local" | 
+  "Hints" | ("Hints" space+ "Resolve") |
+  "Immediate" | "Implicits" | "Import" | 
+  "Infix" | "Load" | "LoadPath" | "Local" | 
   "Match" | "Module" | "Module Type" |
   "Mutual" | "Print" | "Proof" | "Qed" |
-  "Record" | "Recursive" | "Require" | "Save" | "Scheme" |
+  "Record" | "Recursive" | 
+  ("Require" (space+ "Export")? space+ ident) | "Save" | "Scheme" |
   "Section" | "Show" | "Syntactic" | "Syntax" | "Tactic" |
-  "Unset"
-
-let space = 
-  [' ' '\010' '\013' '\009' '\012']
-let firstchar = 
-  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
-let identchar = 
-  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
-let ident = firstchar identchar*
+  "Unset" |
+  ("Set" space+ "Implicit" space+ "Arguments") |
+  ("Implicit" space+ "Arguments" space+ ("On" | "Off"))
 
 let declaration = 
-  "Lemma" | "Axiom" | "CoFixpoint" |"Definition"  |
+  "Lemma" | "Axiom" | "CoFixpoint" | "Definition"  |
+  ("Tactic" space+ "Definition") |
   "Fixpoint" | "Hypothesis" | 
   "Inductive" | "Parameter" | "Remark" |  "Theorem" | 
   "Variable" | "Variables"