From 821937aee71bf9439158e27e06f7b4f74289b209 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 16:57:31 +0200
Subject: STM: proof block detection made optional + simple test

---
 toplevel/coqtop.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 869f6bb931..c52830ea76 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -492,6 +492,10 @@ let parse_args arglist =
         Flags.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
+    |"-async-proofs-tactic-error-resilience" ->
+        Flags.async_proofs_tac_error_resilience := get_bool opt (next ())
+    |"-async-proofs-command-error-resilience" ->
+        Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())
-- 
cgit v1.2.3


From 845dd3dd17b880999a956839c0d84d46de9e27b8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 5 Jun 2016 21:21:43 +0200
Subject: STM: each proof block can be enabled separately

By default we enable only {} and par: that are detectable in
a complete way.
---
 toplevel/coqtop.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c52830ea76..e1f5a70c2a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -379,6 +379,11 @@ let get_host_port opt s =
      prerr_endline ("Error: host:port or stdfds expected after option "^opt);
      exit 1
 
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (String.split ',' s)
+
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
 let vio_tasks = ref []
@@ -493,7 +498,7 @@ let parse_args arglist =
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
     |"-async-proofs-tactic-error-resilience" ->
-        Flags.async_proofs_tac_error_resilience := get_bool opt (next ())
+        Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
     |"-async-proofs-command-error-resilience" ->
         Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
-- 
cgit v1.2.3