From bdcf5b040b975a179fe9b2889fea0d38ae4689df Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Nov 2016 08:38:30 +0100
Subject: Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"

This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.

It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
---
 ide/texmacspp.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index dbcd8630b1..680da7f54b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,6 +724,9 @@ let rec tmpp v loc =
   | VernacComments (cl) ->
       xmlComment loc (List.flatten (List.map pp_comment cl))
 
+  (* Stm backdoor *)
+  | VernacStm _ as x -> xmlTODO loc x
+
   (* Proof management *)
   | VernacGoal _ as x -> xmlTODO loc x
   | VernacAbort _ as x -> xmlTODO loc x
-- 
cgit v1.2.3