- Changement du code de Zplus pour accomoder ring qui sinon prend une

  complexité exponentielle dans la machine lazy depuis que l'algo de
  compilation du filtrage évite systématiquement d'expanser quand le
  filtrage n'est pas dépendant.
- Un peu plus de colorisation dans coqide.
- Utilisation de formats pour améliorer de l'affichage des notations Utf8.
- Systématisation paire Local/Global dans g_vernac.ml4 (même si le
  défaut n'est pas toujours le même)
- Bug Makefile



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

1 files changed, 17 insertions, 4 deletions

diff --git a/ide/highlight.mll b/ide/highlight.mll
index 6649dc31a7..44de2f3581 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -26,7 +26,7 @@
       [  "Add" ; "Check"; "Eval"; "Extraction" ;
 	 "Load" ; "Undo";
 	 "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
-	 "End" ; "Section"
+	 "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
       ];
     Hashtbl.mem h
 
@@ -48,14 +48,14 @@
 	  "Proposition" ; "Property" ;
           (* Definitions *)
 	  "Definition" ; "Let" ; "Example" ; "SubClass" ;
-          "Fixpoint" ; "CoFixpoint"; 
+          "Fixpoint" ; "CoFixpoint" ; "Scheme" ;
           (* Assumptions *)
 	  "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
 	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
           (* Inductive *)
           "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
           (* Other *)
-	  "Ltac" ; "Typeclasses"; "Instance"
+	  "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class"
 	];
       Hashtbl.mem h
 
@@ -73,6 +73,8 @@ let ident = firstchar identchar*
 let multiword_declaration =
   "Module" (space+ "Type")
 | "Program" space+ ident
+| "Existing" space+ "Instance"
+| "Canonical" space+ "Structure"
 
 let locality = ("Local" space+)?
 
@@ -80,14 +82,25 @@ let multiword_command =
   "Set" (space+ ident)* 
 | "Unset" (space+ ident)* 
 | "Open" space+ locality "Scope"
+| "Close" space+ locality "Scope"
+| "Bind" space+ "Scope"
+| "Arguments" space+ "Scope"
+| "Reserved" space+ "Notation" space+ locality
+| "Delimit" space+ "Scope"
 | "Next" space+ "Obligation"
 | "Solve" space+ "Obligations"
-| "Require" space+ ("Import"|"Export")
+| "Require" space+ ("Import"|"Exportp")
 | "Infix" space+ locality
 | "Notation" space+ locality
 | "Hint" space+ locality ident
 | "Reset" (space+ "Initial")?
 | "Tactic" space+ "Notation"
+| "Implicit" space+ "Arguments"
+| "Implicit" space+ ("Type"|"Types")
+| "Combined" space+ "Scheme"
+
+(* At least still missing: "Inline" + decl, variants of "Identity
+  Coercion", variants of Print, Add, ... *)
 
 rule next_starting_order = parse
   | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }