From 1d3ae116e508d29f0760f3e205f0b2e5db1829f8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Oct 2001 12:20:54 +0000
Subject: 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
---
 toplevel/mltop.ml4        |  3 +--
 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 *)
-- 
cgit v1.2.3