aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-01-25 14:39:29 +0100
committerEmilio Jesus Gallego Arias2017-03-21 15:51:49 +0100
commit829a8feb3d02da057d39b5029b422e8a45dd1608 (patch)
treed2caa3d95e3c5462125c54745ed56ba924664dd6 /stm
parent6e3fc0992be7ddd841328028dec51d390fffb851 (diff)
[xml] Restore protocol compatibility with 8.6.
By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds`
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.mllib1
-rw-r--r--stm/workerLoop.ml6
2 files changed, 6 insertions, 1 deletions
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 4b254e8113..72b5380162 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,6 +5,7 @@ TQueue
WorkerPool
Vernac_classifier
CoqworkmgrApi
+WorkerLoop
AsyncTaskQueue
Stm
ProofBlockDelimiter
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 56fcf8537f..50b42512cb 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -6,9 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let rec parse args = args
+let rec parse = function
+ | "--xml_format=Ppcmds" :: rest -> parse rest
+ | x :: rest -> x :: parse rest
+ | [] -> []
let loop init args =
+ let args = parse args in
Flags.make_silent true;
init ();
CoqworkmgrApi.init !Flags.async_proofs_worker_priority;