From ec59306708f9aec04ab82a7e03807017e1924507 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 26 Sep 2017 00:57:41 +0200
Subject: [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.
---
 toplevel/vernac.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4b97ee0dde..b0f021cdcd 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
 
-- 
cgit v1.2.3