Change Dumpglob.pause and Dumpglob.continue into push and pop

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

5 files changed, 39 insertions, 18 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6a6318f97a..5adeafaa38 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -30,6 +30,13 @@ Generic arguments:
 
 - Generic arguments: `wit_var` is deprecated, use `wit_hyp`.
 
+Dumpglob:
+
+- The function `Dumpglob.pause` and `Dumpglob.continue` are replaced
+  by `Dumpglob.push_output` and `Dumpglob.pop_output`. This allows
+  plugins to temporarily change/pause the output of Dumpglob, and then
+  restore it to the original setting.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index d57c05788d..3ec92cf691 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -26,19 +26,29 @@ type glob_output =
   | MultFiles
   | File of string
 
-let glob_output = ref NoGlob
+let glob_output = ref []
 
-let dump () = !glob_output <> NoGlob
+let get_output () = match !glob_output with
+  | [] -> NoGlob
+  | g::_ -> g
 
-let set_glob_output mode =
-  glob_output := mode
+let push_output g = glob_output := g::!glob_output
+
+let pop_output () = glob_output := match !glob_output with
+    | [] -> CErrors.anomaly (Pp.str "No output left to pop")
+    | _::ds -> ds
+
+let pause () = push_output NoGlob
+let continue = pop_output
+
+let dump () = get_output () <> NoGlob
 
 let dump_string s =
-  if dump () && !glob_output != Feedback then
+  if dump () && get_output () != Feedback then
     output_string !glob_file s
 
 let start_dump_glob ~vfile ~vofile =
-  match !glob_output with
+  match get_output () with
   | MultFiles ->
       open_glob_file (Filename.chop_extension vofile ^ ".glob");
       output_string !glob_file "DIGEST ";
@@ -51,14 +61,10 @@ let start_dump_glob ~vfile ~vofile =
       ()
 
 let end_dump_glob () =
-  match !glob_output with
+  match get_output () with
   | MultFiles | File _ -> close_glob_file ()
   | NoGlob | Feedback -> ()
 
-let previous_state = ref MultFiles
-let pause () = previous_state := !glob_output; glob_output := NoGlob
-let continue () = glob_output := !previous_state
-
 open Decls
 open Declarations
 
@@ -141,7 +147,7 @@ let interval loc =
   loc1, loc2-1
 
 let dump_ref ?loc filepath modpath ident ty =
-  match !glob_output with
+  match get_output () with
   | Feedback ->
     Option.iter (fun loc ->
         Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
@@ -247,7 +253,7 @@ let add_glob_kn ?loc kn =
     add_glob_gen ?loc sp lib_dp "syndef"
 
 let dump_def ?loc ty secpath id = Option.iter (fun loc ->
-  if !glob_output = Feedback then
+  if get_output () = Feedback then
     Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
   else
     let bl,el = interval loc in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index be1e3f05d2..857991cb3f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -19,11 +19,19 @@ type glob_output =
   | MultFiles                   (* one glob file per .v file *)
   | File of string              (* Single file for all coqc arguments *)
 
-(* Default "NoGlob" *)
-val set_glob_output : glob_output -> unit
+(** [push_output o] temporarily overrides the output location to [o].
+    The original output can be restored using [pop_output] *)
+val push_output : glob_output -> unit
 
+(** Restores the original output that was overridden by [push_output] *)
+val pop_output : unit -> unit
+
+(** Alias for [push_output NoGlob] *)
 val pause : unit -> unit
+
+(** Deprecated alias for [pop_output] *)
 val continue : unit -> unit
+[@@ocaml.deprecated "Use pop_output"]
 
 val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
 val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0179215d6a..6464556e4e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -108,7 +108,7 @@ let with_full_print f a =
     Constrextern.print_universes := old_printuniverses;
     Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name
       old_printallowmatchdefaultclause;
-    Dumpglob.continue ();
+    Dumpglob.pop_output ();
     res
   with reraise ->
     Impargs.make_implicit_args old_implicit_args;
@@ -118,7 +118,7 @@ let with_full_print f a =
     Constrextern.print_universes := old_printuniverses;
     Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name
       old_printallowmatchdefaultclause;
-    Dumpglob.continue ();
+    Dumpglob.pop_output ();
     raise reraise
 
 (**********************)
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 524f818523..b75a4199ea 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -139,7 +139,7 @@ let compile opts copts ~echo ~f_in ~f_out =
         ~aux_file:(aux_file_name_for long_f_dot_out)
         ~v_file:long_f_dot_in);
 
-      Dumpglob.set_glob_output copts.glob_out;
+      Dumpglob.push_output copts.glob_out;
       Dumpglob.start_dump_glob ~vfile:long_f_dot_in ~vofile:long_f_dot_out;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");