diff options
| author | herbelin | 2001-10-17 12:20:54 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-17 12:20:54 +0000 |
| commit | 1d3ae116e508d29f0760f3e205f0b2e5db1829f8 (patch) | |
| tree | 1a662ba486f127a91f5cc792d704ec7ed67d2f2d | |
| 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
| -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 be6d057b9f..e50af46645 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 d4d51073d9..d37c00b246 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 *) |