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

1 files changed, 19 insertions, 3 deletions

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