Improved monitoring of running proofs

src/ide/gmain.ml

@@ -230,7 +230,7 @@ let cleaning_box =
   ~packing:cleaning_frame#add ()
 
 let monitor_frame =
-  GBin.frame ~label:"Monitor"
+  GBin.frame ~label:"Proof monitoring"
     ~packing:(tools_window_vbox#pack ~expand:false) ()
 
 let monitor_box =

src/ide/replay.ml

@@ -119,7 +119,8 @@ module M = Session.Make
          | None -> timeout_handler := Some(float ms /. 1000.0 ,f);
          | Some _ -> failwith "Replay.timeout: already one handler installed"
 
-     let notify_timer_state _ _ _ = ()
+     let notify_timer_state w s r =
+       Printf.eprintf "Progress: %d/%d/%d   \r%!" w s r 
 
    end)
 
@@ -484,6 +485,7 @@ let () =
     if !opt_latex2 <> "" then print_latex_statistics 2 !opt_latex2
     else 
       let callback report =
+        eprintf "@.";
 	let files,n,m =
           List.fold_left file_statistics ([],0,0) (M.get_all_files ())
 	in

src/ide/session.ml

@@ -447,9 +447,9 @@ let timeout_handler () =
   let continue =
     match l with
       | [] ->
-(**)
+(*
           eprintf "Info: timeout_handler stopped@.";
-(**)
+*)
           false
       | _ -> true
   in
@@ -464,9 +464,9 @@ let run_timeout_handler () =
   if !timeout_handler_activated then () else
     begin
       timeout_handler_activated := true;
-(**)
+(*
       eprintf "Info: timeout_handler started@.";
-(**)
+*)
       O.timeout ~ms:100 timeout_handler
     end
 
@@ -506,9 +506,9 @@ let idle_handler () =
     true
   with Queue.Empty ->
     idle_handler_activated := false;
-(**)
+(*
     eprintf "Info: idle_handler stopped@.";
-(**)
+*)
     false
     | e ->
       Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
@@ -521,9 +521,9 @@ let run_idle_handler () =
   if !idle_handler_activated then () else
     begin
       idle_handler_activated := true;
-(**)
+(*
       eprintf "Info: idle_handler started@.";
-(**)
+*)
       O.idle idle_handler
     end
 
@@ -548,14 +548,15 @@ let cancel_scheduled_proofs () =
         callback Interrupted
       done
     with
-      | Queue.Empty -> ()
+      | Queue.Empty -> 
+          O.notify_timer_state 0 0 (List.length !running_proofs)
 
 
 let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
     ~command ~driver ~callback goal =
-(**)
-  eprintf "Scheduling a new proof attempt@.";
-(**)
+  (*
+    eprintf "Scheduling a new proof attempt@.";
+  *)
   Queue.push
     (Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
                         callback,goal))
@@ -1762,10 +1763,14 @@ let check_all ~callback =
          file.theories)
     !all_files;
   let timeout () =
+(*
     Printf.eprintf "Progress: %d/%d\r%!" !proofs_done !proofs_to_do;
+*)
     if !proofs_done = !proofs_to_do then
       begin
+(*
         Printf.eprintf "\n%!";
+*)
         decr maximum_running_proofs;
         callback !reports;
         false