CoqIDE: show number of proofs being checked in background

good test: Nijmegen/QArithSternBrocot/Zaux.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 31 insertions, 3 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index cb90c0ff08..eb3f09ab7b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -83,6 +83,7 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+  method get_slaves_status : int * int
 
   method handle_failure : handle_exn_rty -> unit task
 
@@ -105,6 +106,10 @@ object(self)
 
   val mutable initial_state = Stateid.initial
 
+  (* proofs being processed by the slaves *)
+  val mutable to_process = 0
+  val mutable processed = 0
+
   val feedbacks : feedback Queue.t = Queue.create ()
   val feedback_timer = Ideutils.mktimer ()
 
@@ -267,6 +272,10 @@ object(self)
           self#attach_tooltip sentence loc msg;
           if not (Loc.is_ghost loc) then
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
+      | InProgress n, _ ->
+          if n < 0 then processed <- processed + abs n
+          else to_process <- to_process + n
+
       | _ ->
           if sentence <> None then Minilib.log "Unsupported feedback message"
           else if Stack.is_empty cmd_stack then ()
@@ -378,6 +387,8 @@ object(self)
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
 
+  method get_slaves_status = processed, to_process
+
   method process_next_phrase =
     let until len start stop = 1 <= len in
     let next () =
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index d286ad3d17..5816ef86e5 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -21,6 +21,7 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+  method get_slaves_status : int * int
 
   method handle_failure : Interface.handle_exn_rty -> unit task
   
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 888f07128b..2decc42b94 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1246,13 +1246,29 @@ let build_ui () =
   let () = set_location := l#set_text in
 
   (* Progress Bar *)
-  let pbar = GRange.progress_bar ~pulse_step:0.2 () in
+  let pbar = GRange.progress_bar ~pulse_step:0.1 () in
   let () = lower_hbox#pack pbar#coerce in
-  let () = pbar#set_text "CoqIde started" in
-  let pulse sn = if Coq.is_computing sn.coqtop then pbar#pulse () in
+  let ready () = pbar#set_fraction 0.0; pbar#set_text "Coq is ready" in
+  let pulse sn =
+    if Coq.is_computing sn.coqtop then
+      (pbar#set_text "Coq is working"; pbar#pulse ())
+    else ready () in
   let callback () = on_current_term pulse; true in
   let _ = Glib.Timeout.add ~ms:300 ~callback in
 
+  (* Pending proofs *)
+  let pbar = GRange.progress_bar ~pulse_step:0.1 () in
+  let () = lower_hbox#pack pbar#coerce in
+  let txt n = pbar#set_text ("To check: " ^ string_of_int n) in
+  let update sn =
+    let processed, to_process = sn.coqops#get_slaves_status in
+    let missing = to_process - processed in
+    if missing = 0 then
+      (pbar#set_text "All checked";pbar#set_fraction 0.0)
+    else (pbar#pulse (); txt missing) in
+  let callback () = on_current_term update; true in
+  let _ = Glib.Timeout.add ~ms:300 ~callback in
+
   (* Initializing hooks *)
   let refresh_toolbar () =
     if prefs.show_toolbar