From cf6b12cb3a88fb3af6a7b3e91d17db8b06d23c81 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 1 Sep 2014 14:54:49 +0200
Subject: coqworkmgr

---
 toplevel/coqtop.ml | 11 ++++++++++-
 toplevel/vernac.ml |  5 +++++
 2 files changed, 15 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 43ffa762e2..b418269955 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -41,7 +41,9 @@ let print_header () =
 let warning s = msg_warning (strbrk s)
 
 let toploop = ref None
-let toploop_init = ref (fun x -> x)
+let toploop_init = ref (fun x ->
+  CoqworkmgrApi.(init !Flags.async_proofs_worker_priority);
+  x)
 let toploop_run = ref (fun () ->
   if Dumpglob.dump () then begin
     if_verbose warning "Dumpglob cannot be used in interactive mode.";
@@ -228,6 +230,11 @@ let no_compat_ntn = ref false
 let print_where = ref false
 let print_config = ref false
 
+let get_priority opt s =
+  try Flags.priority_of_string s
+  with Invalid_argument _ ->
+    prerr_endline ("Error: low/high expected after "^opt); exit 1
+
 let get_async_proofs_mode opt = function
   | "off" -> Flags.APoff
   | "on" -> Flags.APon
@@ -359,6 +366,8 @@ let parse_args arglist =
         Flags.async_proofs_n_workers := (get_int opt (next ()))
     |"-async-proofs-tac-j" ->
         Flags.async_proofs_n_tacworkers := (get_int opt (next ()))
+    |"-async-proofs-worker-priority" ->
+        Flags.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
     |"-worker-id" -> set_worker_id opt (next ())
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a011fc6a69..5e9d77bedd 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -350,3 +350,8 @@ let compile verbosely f =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv lib univs proofs
 
+let compile v f = 
+  ignore(CoqworkmgrApi.get 1);
+  compile v f;
+  CoqworkmgrApi.giveback 1
+
-- 
cgit v1.2.3