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.
---
 printing/ppvernac.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a6b1c97f5c..3494ad006f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,6 +538,22 @@ module Make
       | VernacLocal (local, v) ->
         return (pr_locality local ++ spc() ++ pr_vernac_body v)
 
+      (* Stm *)
+      | VernacStm JoinDocument ->
+        return (keyword "Stm JoinDocument")
+      | VernacStm PrintDag ->
+        return (keyword "Stm PrintDag")
+      | VernacStm Finish ->
+        return (keyword "Stm Finish")
+      | VernacStm Wait ->
+        return (keyword "Stm Wait")
+      | VernacStm (Observe id) ->
+        return (keyword "Stm Observe " ++ str(Stateid.to_string id))
+      | VernacStm (Command v) ->
+        return (keyword "Stm Command " ++ pr_vernac_body v)
+      | VernacStm (PGLast v) ->
+        return (keyword "Stm PGLast " ++ pr_vernac_body v)
+
       (* Proof management *)
       | VernacAbortAll ->
         return (keyword "Abort All")
-- 
cgit v1.2.3