From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Oct 2017 19:21:00 +0200
Subject: [stm] First step to move interpretation of Undo commands out of the
 classifier.

The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.

We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
---
 intf/vernacexpr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index bc7146884c..3cb1a311f8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -503,6 +503,7 @@ type vernac_type =
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * Feedback.route_id
   | VtBack of vernac_part_of_script * Stateid.t
+  | VtMeta
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
-- 
cgit v1.2.3


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.
---
 intf/vernacexpr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 3cb1a311f8..ea412a7d6a 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -502,7 +502,6 @@ type vernac_type =
   | VtProofStep of proof_step
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * Feedback.route_id
-  | VtBack of vernac_part_of_script * Stateid.t
   | VtMeta
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-- 
cgit v1.2.3