** 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

1 files changed, 13 insertions, 11 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 59da90e66..0b0483a85 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -81,19 +81,26 @@ let openmod_info =
   ref (([],None,None) : mod_bound_id list * module_struct_entry option 
                                           * struct_expr_body option) 
 
+(* The library_cache here is needed to avoid recalculations of
+   substituted modules object during "reloading" of libraries *)
+let library_cache = ref Dirmap.empty
+
 let _ = Summary.declare_summary "MODULE-INFO"
 	  { Summary.freeze_function = (fun () -> 
 					 !modtab_substobjs,
 					 !modtab_objects,
-					 !openmod_info);
-	    Summary.unfreeze_function = (fun (sobjs,objs,info) -> 
+					 !openmod_info,
+					 !library_cache);
+	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> 
 					   modtab_substobjs := sobjs;
 					   modtab_objects := objs;
-					   openmod_info := info);
+					   openmod_info := info;
+					   library_cache := libcache);
 	    Summary.init_function = (fun () -> 
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
-				       openmod_info := ([],None,None));
+				       openmod_info := ([],None,None);
+				       library_cache := Dirmap.empty);
 	    Summary.survive_module = false;
 	    Summary.survive_section = false }
 
@@ -729,18 +736,13 @@ type library_objects =
     mod_self_id * lib_objects * lib_objects
 
 
-(* The library_cache here is needed to avoid recalculations of
-   substituted modules object during "reloading" of libraries *)
-let library_cache = Hashtbl.create 17
-
-
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
   let substobjs, objects =
     try 
       ignore(Global.lookup_module mp);
       (* if it's in the environment, the cached objects should be correct *)
-      Hashtbl.find library_cache dir
+      Dirmap.find dir !library_cache 
     with
 	Not_found ->
 	  if mp <> Global.import cenv digest then
@@ -750,7 +752,7 @@ let register_library dir cenv objs digest =
 	  let substituted = subst_substobjs dir mp substobjs in
 	  let objects = Option.map (fun seg -> seg@keep) substituted in
 	  let modobjs = substobjs, objects in
-	    Hashtbl.add library_cache dir modobjs;
+	    library_cache := Dirmap.add dir modobjs !library_cache;
 	    modobjs
   in
     do_module false "register_library" load_objects 1 dir mp substobjs objects