[stm] Warn about costly Undo operations in batch mode [BZ#5677]

Undo & friends is very expensive in batch mode as backtracking state
is not kept and thus should be recomputed.

We thus warn the user.

1 files changed, 6 insertions, 0 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4b97ee0dd..b0f021cdc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -132,10 +132,16 @@ let rec interp_vernac sid (loc,com) =
          highly dynamic and depends on the structure of the
          document. Hopefully this is fixed when VtBack can be removed
          and Undo etc... are just interpreted regularly. *)
+
+      (* XXX: The classifier can emit warnings so we need to guard
+         against that... *)
+      let wflags = CWarnings.get_flags () in
+      CWarnings.set_flags "none";
       let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
         | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
         | _ -> false
       in
+      CWarnings.set_flags wflags;
 
       let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in