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

6 files changed, 41 insertions, 4 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
diff --git a/lib/interface.mli b/lib/interface.mli
index 560d80d83f..144b98252b 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -125,6 +125,7 @@ type feedback_content =
   | Processed
   | GlobRef of Loc.t * string * string * string * string
   | ErrorMsg of Loc.t * string
+  | InProgress of int
 
 type feedback = {
   id : edit_or_state_id;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 5c818ad614..c1933ad90c 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -605,6 +605,10 @@ let to_feedback_content xml = do_match xml "feedback_content"
        (match args with
        | [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
        | _ -> raise Marshal_error)
+  | "inprogress" -> 
+       (match args with
+       | [n] -> InProgress (to_int n)
+       | _ -> raise Marshal_error)
   | _ -> raise Marshal_error)
 
 let of_feedback_content = function
@@ -620,6 +624,7 @@ let of_feedback_content = function
     ]
 | ErrorMsg(loc, s) ->
     constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
+| InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 67e855327b..9310591416 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -631,7 +631,9 @@ end = struct (* {{{ *)
   let build_proof_here (id,valid) eop =
     Future.create (fun () ->
       !reach_known_state ~cache:false eop;
-      Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid))
+      let p = Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid) in
+      Pp.feedback (Interface.InProgress ~-1);
+      p)
 
   let slave_respond msg =
     match msg with
@@ -680,6 +682,7 @@ end = struct (* {{{ *)
       build_proof_here exn_info stop
     else 
       let f, assign = Future.create_delegate () in
+      Pp.feedback (Interface.InProgress 1);
       TQueue.push queue (TaskBuildProof(exn_info,start,stop,assign));
       f