aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-17 12:20:54 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-17 12:20:54 +0000
commit1d3ae116e508d29f0760f3e205f0b2e5db1829f8 (patch)
tree1a662ba486f127a91f5cc792d704ec7ed67d2f2d /toplevel
parentda99ba17909124a9fdc3ce1684dd381595522554 (diff)
Amélioration mise en page Print ML Module et Print ML Module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2124 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/mltop.ml43
-rw-r--r--toplevel/vernacentries.ml12
2 files changed, 7 insertions, 8 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index be6d057b9..e50af4664 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -297,5 +297,4 @@ let print_ml_path () =
let print_ml_modules () =
let l = get_loaded_modules () in
- pP [< 'sTR"Loaded ML Modules : " ;
- hOV 0 (prlist_with_sep pr_fnl pr_str l); 'fNL >]
+ pP [< 'sTR"Loaded ML Modules: " ; pr_vertical_list pr_str l >]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d4d51073d..d37c00b24 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -363,12 +363,12 @@ let _ =
(fun () ->
let opened = Library.opened_modules ()
and loaded = Library.loaded_modules () in
- mSG [< 'sTR"Loaded Modules: ";
- hOV 0 (prlist_with_sep pr_fnl pr_dirpath loaded);
- 'fNL;
- 'sTR"Imported (open) Modules: ";
- hOV 0 (prlist_with_sep pr_fnl pr_dirpath opened);
- 'fNL >])
+ let loaded_opened = list_intersect loaded opened
+ and only_loaded = list_subtract loaded opened in
+ mSG [< 'sTR"Loaded and imported modules: ";
+ pr_vertical_list pr_dirpath loaded_opened; 'fNL;
+ 'sTR"Loaded and not imported modules: ";
+ pr_vertical_list pr_dirpath only_loaded >])
| _ -> bad_vernac_args "PrintModules")
(* Sections *)