From efb37cb4dd0976acd2a87c6a27d1fb3e9e80ad30 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Mar 2018 00:49:56 +0100
Subject: [stm] Never consider `Backtrack` as part of the script.

This makes Emacs's `Backtrack` commands to be similar to `EditAt`,
thus they will correctly revert the document state. This fixes #6240
and likely some other synchronization bugs.

It is still unfortunate that true meta commands are part of the
vernacular, we should fix this for 8.9.
---
 stm/stm.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index ad94b68077..dbecbdae54 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2803,6 +2803,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       (* Meta *)
       | VtMeta, _ ->
         let id, w = Backtrack.undo_vernac_classifier expr in
+        (* Special case Backtrack, as it is never part of a script. See #6240 *)
+        let part_of_script = begin match Vernacprop.under_control expr with
+          | VernacBacktrack _ -> false
+          | _ -> part_of_script
+        end in
         process_back_meta_command ~part_of_script ~newtip ~head id x w
       (* Query *)
       | VtQuery (false,route), VtNow ->
-- 
cgit v1.2.3