From d9704f80a4f4b565f77368dbf7c9650d301a233d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Oct 2017 12:54:57 +0200 Subject: [stm] Remove VtBack from public classification. We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away. --- toplevel/vernac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d736975d3..cf63fbdc3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -119,7 +119,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtBack can be removed + document. Hopefully this is fixed when VtMeta can be removed and Undo etc... are just interpreted regularly. *) (* XXX: The classifier can emit warnings so we need to guard @@ -127,7 +127,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = 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 + | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; -- cgit v1.2.3