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, 17 insertions, 0 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8b41ba038..904db670f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -173,6 +173,21 @@ let print_modules () =
   str"Loaded and not imported modules: " ++
   pr_vertical_list pr_dirpath only_loaded
 
+
+let print_module (loc,qid) =
+  try
+    let mp = Nametab.locate_module qid in
+      msgnl (Printmod.print_module true mp)
+  with
+      Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid)
+
+let print_modtype (loc,qid) = 
+  try
+    let kn = Nametab.locate_modtype qid in
+      msgnl (Printmod.print_modtype kn)
+  with
+      Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid)
+
 let dump_universes s =
   let output = open_out s in
   try
@@ -792,6 +807,8 @@ let vernac_print = function
   | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent
   | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
   | PrintModules -> msg (print_modules ())
+  | PrintModule qid -> print_module qid
+  | PrintModuleType qid -> print_modtype qid
   | PrintMLLoadPath -> Mltop.print_ml_path ()
   | PrintMLModules -> Mltop.print_ml_modules ()
   | PrintName qid ->