aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofworkertop.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-30 17:47:07 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-31 15:54:00 +0100
commite6afe851f90c8a864c20fe287ee3a7d5e03c8b77 (patch)
tree066a6a28a8493819f1ee02f31d9f8a27bb96f82e /stm/proofworkertop.ml
parentbaef2bd34e1906ab56918c37a90c5468a4785656 (diff)
STM: reorganize code and file names
- proofworkertop to deal with proof tasks - tacworkertop to deal with par: tactics - queryworkertop to deal with queries (next commit)
Diffstat (limited to 'stm/proofworkertop.ml')
-rw-r--r--stm/proofworkertop.ml16
1 files changed, 16 insertions, 0 deletions
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
new file mode 100644
index 000000000..0d1b44e49
--- /dev/null
+++ b/stm/proofworkertop.ml
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+let () = Coqtop.toploop_init := (fun args ->
+ Flags.make_silent true;
+ Stm.slave_init_stdout ();
+ CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+ args)
+
+let () = Coqtop.toploop_run := Stm.slave_main_loop
+