Suite commit 11236

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11240 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 15 insertions, 10 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index b8121af866..ca817b776b 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -25,23 +25,26 @@ let dump_string s =
   Pervasives.output_string !glob_file s
 
 type glob_output_t = 
-    | None
+    | NoGlob
     | StdOut
     | MultFiles
     | File of string
 
-let glob_output = ref MultFiles
+let glob_output = ref NoGlob
 
-let dump () = !glob_output != None
+let dump () = !glob_output != NoGlob
 
-let noglob () = glob_output := None
+let noglob () = glob_output := NoGlob
 
-let dump_to_stdout () = glob_output := StdOut
+let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
 
 let multi_dump () = !glob_output = MultFiles
 
+let dump_to_dotglob f = glob_output := MultFiles
+
 let dump_into_file f = glob_output := File f; open_glob_file f
 
+
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output
 let continue () = glob_output := !previous_state
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1a856d477d..7567f0eb6f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -177,8 +177,10 @@ let usage () =
 
 let warning s = msg_warning (str s)
 
+
 let ide_args = ref []
 let parse_args is_ide =
+  let glob_opt = ref false in
   let rec parse = function
     | [] -> ()
     | "-with-geoproof" :: s :: rem -> 
@@ -240,20 +242,20 @@ let parse_args is_ide =
     | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
-    | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); parse rem
+    | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
 	  (* À ne pas documenter : l'option 'stdout' n'étant
 	     éventuellement utile que pour le debugging... *)
-    | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; parse rem
+    | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
     | "-dump-glob" :: []       -> usage ()
-    | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); parse rem
+    | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
 
     | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
 
-    | "-compile" :: f :: rem -> add_compile false f; parse rem
+    | "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
     | "-compile" :: []       -> usage ()
 
-    | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
+    | "-compile-verbose" :: f :: rem -> add_compile true f;  if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
     | "-compile-verbose" :: []       -> usage ()
 
     | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem