** Efficacité, bugs, robustesse CoqIDE **

- Suppression d'une source de fuite mémoire dans declare_mod.ml (la
  table de hash library_table n'était pas synchronisée avec le reset
  et elle grossissait à chaque rejeu de la session; utilisation au
  passage d'une map pour que la synchronisation avec le reset soit
  plus rapide). [mod_typing.ml]

- Correction d'un bug de synchronisation pour le niveau pattern 200.
  [pcoq.ml4]

- Suppression d'un vieux reste du traducteur [constructeur VernacVar]

- Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de
  chacune des commandes vernaculaires par l'utilisation d'une fonction
  d'assignation d'attributs à chaque commande vernac.

  Correction de ce qui semble être des bizarreries
  (VernacDeclareTacticDefinition considéré comme ouvrant un but;
  suppression des "loc" dans les Reset: ne pouvait pas faire
  fonctionner correctement update_on_end_of_segment).

  Suppression de la nécessité d'expliciter si une commande retourne
  des messages dépendants du mode "verbose" (on suppose que chaque
  commande sait ce qu'elle doit dire selon la position du flag verbose).

  Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne
  sait revenir qu'aux états associés à des noms et cela ne vaut pas
  l'approche de Proof General. Il sera sans doute opportun de se
  brancher sur l'architecture de Pierre Courtieu à base de "Backtrack".

  La restriction des buts imbriqués a-t-elle vraiment une raison
  d'être ? En plus les commandes non cablées en dur comme Next
  Obligation ne sont pas prises en compte.

  Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours.

  Réparation approximative de l'option "Help for Keyword" de Coqide
  mais encore à faire pour plus de robustesse (makefile, installation,
  synchronisation entre la version du fichier index_urls.txt et la
  version du refman, ...).



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

2 files changed, 10 insertions, 8 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 387c727450..481b73fd0c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -78,18 +78,21 @@ let grammar_delete e pos reinit rls =
 
       (* Caveat: deletion is not the converse of extension: when an
 	 empty level is extended, deletion removes the level instead
-	 of keeping it empty. This has an effect on the empty levels 8
-	 and 99. We didn't find a good solution to this problem
+	 of keeping it empty. This has an effect on the empty levels 8,
+	 99 and 200. We didn't find a good solution to this problem
 	 (e.g. using G.extend to know if the level exists results in a
 	 printed error message as side effect). As a consequence an
-	 extension at 99 or 8 inside a section corrupts the parser. *)
+	 extension at 99 or 8 (and for pattern 200 too) inside a section 
+         corrupts the parser. *)
 
       List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
     (List.rev rls);
   if reinit <> None then
     let lev = match pos with Some (Gramext.Level n) -> n | _ -> assert false in
-    G.extend e (Some (Gramext.After (string_of_int (int_of_string lev + 1))))
-      [Some lev,reinit,[]];
+    let pos =
+      if lev = "200" then Gramext.First 
+      else Gramext.After (string_of_int (int_of_string lev + 1)) in
+    G.extend e (Some pos) [Some lev,reinit,[]];
 
 (* grammar_object is the superclass of all grammar entries *)
 module type Gramobj =
@@ -528,7 +531,7 @@ END
    (to be translated into "constr LEVEL n") 
 
    The boolean is true if the entry was existing _and_ empty; this to
-   circumvent a weakness of camlp5 whose undo mechanism is not the
+   circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
    converse of the extension mechanism *)
 
 let constr_level = string_of_int
@@ -545,7 +548,7 @@ let default_levels =
    0,Gramext.RightA,false]
 
 let default_pattern_levels =
-  [200,Gramext.RightA,false;
+  [200,Gramext.RightA,true;
    100,Gramext.RightA,false;
    99,Gramext.RightA,true;
    10,Gramext.LeftA,false;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 352f58f6ba..535a4c380b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -468,7 +468,6 @@ let rec pr_vernac = function
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
   ++ spc()) else spc()  ++ qs s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
-  | VernacVar id -> pr_lident id
   
   (* Syntax *) 
   | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)