From 61f4df8b5b974302e8b48bcf271aa68757db69fe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 8 Aug 2019 23:15:19 +0200
Subject: [glob/aux files] Remove undocumented Stdout dump, cleanup flags.

Fixes #10640

We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.

No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.

Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
---
 interp/dumpglob.ml | 32 +++++++++++---------------------
 1 file changed, 11 insertions(+), 21 deletions(-)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 8d6a266c30..41d1da9694 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -20,31 +20,21 @@ let open_glob_file f =
 let close_glob_file () =
   close_out !glob_file
 
-type glob_output_t =
-    | NoGlob
-    | StdOut
-    | MultFiles
-    | Feedback
-    | File of string
+type glob_output =
+  | NoGlob
+  | Feedback
+  | MultFiles
+  | File of string
 
 let glob_output = ref NoGlob
 
-let dump () = !glob_output != NoGlob
+let dump () = !glob_output <> NoGlob
 
-let noglob () = glob_output := NoGlob
-
-let dump_to_dotglob () = glob_output := MultFiles
-
-let dump_into_file f =
-  if String.equal f "stdout" then
-    (glob_output := StdOut; glob_file := stdout)
-  else
-    (glob_output := File f; open_glob_file f)
-
-let feedback_glob () = glob_output := Feedback
+let set_glob_output mode =
+  glob_output := mode
 
 let dump_string s =
-  if dump () && !glob_output != Feedback then 
+  if dump () && !glob_output != Feedback then
     output_string !glob_file s
 
 let start_dump_glob ~vfile ~vofile =
@@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile =
   | File f ->
       open_glob_file f;
       output_string !glob_file "DIGEST NO\n"
-  | NoGlob | Feedback | StdOut ->
+  | NoGlob | Feedback ->
       ()
 
 let end_dump_glob () =
   match !glob_output with
   | MultFiles | File _ -> close_glob_file ()
-  | NoGlob | Feedback | StdOut -> ()
+  | NoGlob | Feedback -> ()
 
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
-- 
cgit v1.2.3