[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.

1 files changed, 5 insertions, 0 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ad94b6807..dbecbdae5 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 ->