diff options
author | 2001-10-17 12:20:54 +0000 | |
---|---|---|
committer | 2001-10-17 12:20:54 +0000 | |
commit | 1d3ae116e508d29f0760f3e205f0b2e5db1829f8 (patch) | |
tree | 1a662ba486f127a91f5cc792d704ec7ed67d2f2d /toplevel | |
parent | da99ba17909124a9fdc3ce1684dd381595522554 (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.ml4 | 3 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 12 |
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 *) |