Pretty-printing preliminaire des modules, commandes

Print Module qid.
Print Module Type qid.
et affichage pendant
Print All.

Tout ca est preliminare, seuls les noms des composants sont affiches et
non pas les corps...


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

1 files changed, 46 insertions, 14 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 1f8111a2c..5e1464f10 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -46,10 +46,17 @@ module Globtab = Map.Make(struct type t=extended_global_reference
 				 let compare = compare end)
 
 type globtab = section_path Globtab.t
-
 let the_globtab = ref (Globtab.empty : globtab)
 
 
+type mprewtab = dir_path MPmap.t
+let the_modrewtab = ref (MPmap.empty : mprewtab)
+
+
+type knrewtab = section_path KNmap.t
+let the_modtyperewtab = ref (KNmap.empty : knrewtab)
+
+
 let sp_of_global ctx_opt ref = 
   match (ctx_opt,ref) with
     | Some ctx, VarRef id -> 
@@ -194,7 +201,9 @@ let push_syntactic_definition visibility sp kn =
 
 let push = push_cci
 
-let push_modtype vis sp kn = push_idtree the_modtypetab vis sp (kn,sp)
+let push_modtype vis sp kn = 
+  push_idtree the_modtypetab vis sp (kn,sp);
+  the_modtyperewtab := KNmap.add kn sp !the_modtyperewtab
 
 
 (* This is for dischargeable non-cci objects (removed at the end of the
@@ -208,8 +217,11 @@ let push_object visibility sp =
 let push_tactic = push_object
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
-let push_dir = push_modidtree the_dirtab
-
+let push_dir vis dir dir_ref = 
+  push_modidtree the_dirtab vis dir dir_ref;
+  match dir_ref with
+      DirModule (_,(mp,_)) -> the_modrewtab := MPmap.add mp dir !the_modrewtab
+    | _ -> ()
 
 (* As before we start with generic functions *)
 
@@ -346,17 +358,30 @@ let exists_modtype sp =
 
 (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x
    and Coq.A.B.x is a qualid that denotes the same object. *)
-let shortest_qualid_of_global env ref =  
-  let sp = sp_of_global env ref in
-  let (pth,id) = repr_path sp in
+let shortest_qualid locate ref dir_path id =  
   let rec find_visible dir qdir =
     let qid = make_qualid qdir id in
     if (try locate qid = ref with Not_found -> false) then qid
     else match dir with
-      | [] -> qualid_of_sp sp
+      | [] -> make_qualid dir_path id
       | a::l -> find_visible l (add_dirpath_prefix a qdir)
   in
-  find_visible (repr_dirpath pth) (make_dirpath [])
+  find_visible (repr_dirpath dir_path) empty_dirpath
+
+let shortest_qualid_of_global env ref = 
+  let sp = sp_of_global env ref in
+  let (pth,id) = repr_path sp in
+    shortest_qualid locate ref pth id
+
+let shortest_qualid_of_module mp = 
+  let dir = MPmap.find mp !the_modrewtab in
+  let dir,id = split_dirpath dir in
+    shortest_qualid locate_module mp dir id
+
+let shortest_qualid_of_modtype kn =
+  let sp = KNmap.find kn !the_modtyperewtab in
+  let dir,id = repr_path sp in
+    shortest_qualid locate_modtype kn dir id
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
@@ -377,28 +402,35 @@ let global_inductive (loc,qid as locqid) =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * objtab * knsptab * globtab
+type frozen = ccitab * dirtab * objtab * knsptab 
+    * globtab * mprewtab * knrewtab
 
 let init () = 
   the_ccitab := Idmap.empty; 
   the_dirtab := ModIdmap.empty;
   the_objtab := Idmap.empty;
   the_modtypetab := Idmap.empty;
-  the_globtab := Globtab.empty
+  the_globtab := Globtab.empty;
+  the_modrewtab := MPmap.empty;
+  the_modtyperewtab := KNmap.empty
 
 let freeze () =
   !the_ccitab, 
   !the_dirtab,
   !the_objtab,
   !the_modtypetab,
-  !the_globtab
+  !the_globtab,
+  !the_modrewtab,
+  !the_modtyperewtab
 
-let unfreeze (mc,md,mo,mt,gt) =
+let unfreeze (mc,md,mo,mt,gt,mrt,mtrt) =
   the_ccitab := mc;
   the_dirtab := md;
   the_objtab := mo;
   the_modtypetab := mt;
-  the_globtab := gt
+  the_globtab := gt;
+  the_modrewtab := mrt;
+  the_modtyperewtab := mtrt
 
 let _ = 
   Summary.declare_summary "names"