[stm] Move VernacBacktrack to the toplevel.

This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.

1 files changed, 7 insertions, 0 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 64d839f18b..371be20d25 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -338,6 +338,13 @@ let rec vernac_loop ~state =
   try
     let input = top_buffer.tokens in
     match read_sentence ~state input with
+    | {v=VernacBacktrack(bid,_,_)} ->
+      let bid = Stateid.of_int bid in
+      let doc, res = Stm.edit_at ~doc:state.doc bid in
+      assert (res = `NewTip);
+      let state = { state with doc; sid = bid } in
+      vernac_loop ~state
+
     | {v=VernacQuit} ->
       exit 0
     | {v=VernacDrop} ->