CoqIDE: new async error reporting window and slaves status

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

3 files changed, 119 insertions, 16 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb3f09ab7..4ce552928 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -11,7 +11,11 @@ open Coq
 open Ideutils
 open Interface
 
-type flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ]
+type flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR of string ]
+type mem_flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ]
+let mem_flag_of_flag : flag -> mem_flag = function
+  | `ERROR _ -> `ERROR
+  | (`COMMENT | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
 
 module SentenceId : sig
 
@@ -29,7 +33,8 @@ module SentenceId : sig
   val assign_state_id : sentence -> Stateid.t -> unit
   val set_flags : sentence -> flag list -> unit
   val add_flag : sentence -> flag -> unit
-  val remove_flag : sentence -> flag -> unit
+  val has_flag : sentence -> mem_flag -> bool
+  val remove_flag : sentence -> mem_flag -> unit
   val same_sentence : sentence -> sentence -> bool
   val hidden_edit_id : unit -> int
 
@@ -59,7 +64,10 @@ end = struct
     s.state_id <- Some id
   let set_flags s f = s.flags <- f
   let add_flag s f = s.flags <- CList.add_set f s.flags
-  let remove_flag s f = s.flags <- CList.remove f s.flags
+  let has_flag s mf =
+    List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
+  let remove_flag s mf =
+    s.flags <- List.filter (fun f -> mem_flag_of_flag f = mf) s.flags
   let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id
 
 end
@@ -83,6 +91,9 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+
+  method get_n_errors : int
+  method get_errors : (int * string) list
   method get_slaves_status : int * int
 
   method handle_failure : handle_exn_rty -> unit task
@@ -116,7 +127,7 @@ object(self)
   initializer
     Coq.set_feedback_handler _ct self#enqueue_feedback;
     Wg_Tooltip.set_tooltip_callback (script :> GText.view);
-    feedback_timer.Ideutils.run ~ms:250 ~callback:self#process_feedback
+    feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback
 
   method destroy () =
     feedback_timer.Ideutils.kill ()
@@ -202,8 +213,8 @@ object(self)
     let error_bg = Tags.Script.error_bg in
     let all_tags = [ to_process; processed; unjustified ] in
     let tags =
-      (if List.mem `PROCESSING sentence.flags then to_process else
-       if List.mem `ERROR sentence.flags then error_bg else
+      (if has_flag sentence `PROCESSING then to_process else
+       if has_flag sentence `ERROR then error_bg else
        processed)
       ::
       (if [ `UNSAFE ] = sentence.flags then [unjustified] else [])
@@ -267,7 +278,7 @@ object(self)
       | ErrorMsg(loc, msg), Some sentence ->
           log "ErrorMsg" sentence;
           remove_flag sentence `PROCESSING;
-          add_flag sentence `ERROR;
+          add_flag sentence (`ERROR msg);
           self#mark_as_needed sentence;
           self#attach_tooltip sentence loc msg;
           if not (Loc.is_ghost loc) then
@@ -352,7 +363,7 @@ object(self)
         let sentence = Queue.pop queue in
         add_flag sentence `PROCESSING;
         Stack.push sentence cmd_stack;
-        if List.mem `COMMENT sentence.flags then
+        if has_flag sentence `COMMENT then
           let () = remove_flag sentence `PROCESSING in
           let () = self#commit_queue_transaction sentence in
           loop ()
@@ -389,6 +400,21 @@ object(self)
 
   method get_slaves_status = processed, to_process
 
+  method get_n_errors = 
+    List.fold_left
+      (fun n s -> if has_flag s `ERROR then n+1 else n)
+      0 (Stack.to_list cmd_stack)
+
+  method get_errors =
+    let extract_error s =
+      match List.find (function `ERROR _ -> true | _ -> false) s.flags with
+      | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg
+      | _ -> assert false in
+    CList.map_filter (fun s ->
+      if has_flag s `ERROR then Some (extract_error s)
+      else None)
+      (Stack.to_list cmd_stack)
+
   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 5816ef86e..e313cd47a 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -21,8 +21,12 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+
+  method get_n_errors : int
+  method get_errors : (int * string) list
   method get_slaves_status : int * int
 
+
   method handle_failure : Interface.handle_exn_rty -> unit task
   
   method destroy : unit -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2decc42b9..9ea523c73 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1251,21 +1251,94 @@ let build_ui () =
   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 ())
+      (pbar#set_text "Coq is computing"; 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
+  (* Pending proofs.  It should be with a GtkSpinner... not bound *)
+  let slaveinfobut = GButton.button () in
+  let slaveinfo = GMisc.label ~xalign:0.5 ~width:50 () in
+  let () = lower_hbox#pack slaveinfobut#coerce in
+  let () = slaveinfobut#add slaveinfo#coerce in
+  let () = slaveinfobut#misc#set_has_tooltip true in
+  let () = slaveinfobut#misc#set_tooltip_markup
+    "Proofs to be checked / Errors" in
+  let errwin, fill_errwin =
+    let obj = GWindow.window ~title:"Errors" ~deletable:true
+      ~position:`CENTER_ON_PARENT ~show:false ~width:400 ~height:300 () in
+    let vb = GPack.vbox ~homogeneous:false ~packing:obj#add () in
+    let frame = GBin.scrolled_window
+      ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in
+    let tip = GMisc.label ~text:"Double click to jump to error line" () in
+    let () = vb#pack ~expand:true frame#coerce in
+    let () = vb#pack ~expand:false ~padding:2 tip#coerce in
+    let cols = new GTree.column_list in
+    let column1 = cols#add Gobject.Data.int in
+    let column2 = cols#add Gobject.Data.string in
+    let column3 = cols#add Gobject.Data.int in
+    let store = GTree.list_store cols in
+    let data = GTree.view
+      ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment
+      ~rules_hint:true ~headers_visible:false
+      ~model:store ~packing:frame#add () in
+    let () = data#set_headers_visible true in
+    let renderer1 = GTree.cell_renderer_text [], ["text", column1] in
+    let col1 = GTree.view_column ~renderer:renderer1 () in
+    let () = col1#set_title "Line" in
+    let renderer2 = GTree.cell_renderer_text [], ["text", column2] in
+    let col2 = GTree.view_column ~renderer:renderer2 () in
+    let () = col2#set_title "Error message" in
+    let renderer3 = GTree.cell_renderer_text [], ["text", column3] in
+    let col3 = GTree.view_column ~renderer:renderer3 () in
+    let () = col3#set_title "Hidden tab number" in
+    let () = col3#set_visible false in
+    let _ = data#append_column col1 in
+    let _ = data#append_column col2 in
+    let _ = data#append_column col3 in
+    let () = col1#set_sizing `AUTOSIZE in
+    let () = col2#set_sizing `AUTOSIZE in
+    let _ = data#connect#row_activated ~callback:(fun tp vc -> 
+      let row = store#get_iter tp in
+      let lno = store#get ~row ~column:column1 in
+      let tabno = store#get ~row ~column:column3 in
+      let sn = notebook#get_nth_term tabno in
+      ignore(sn.script#scroll_to_iter
+        ~use_align:false ~yalign:0.75 ~within_margin:0.25
+        (sn.script#buffer#get_iter (`LINE (lno-1))))) in
+    obj, (let last_update = ref (0,[]) in
+          fun tabno l ->
+            if !last_update = (tabno,l) then ()
+            else begin
+              last_update := tabno,l;
+              store#clear ();
+              List.iter (fun (lno, msg) ->
+                let line = store#append () in
+                store#set line column1 lno;
+                store#set line column2 msg;
+                store#set line column3 tabno) l
+            end)
+  in
+  let () = errwin#set_transient_for w#as_window in
+  let _ = errwin#event#connect#delete
+    ~callback:(fun _ -> errwin#misc#hide (); true) in
+  let update_errwin () =
+    on_current_term (fun sn ->
+      fill_errwin (notebook#term_num (==) sn) sn.coqops#get_errors) in
+  let _ = slaveinfobut#connect#clicked ~callback:(fun () ->
+     update_errwin ();
+     errwin#misc#show ()) 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 n_err = sn.coqops#get_n_errors in
+    if n_err > 0 then
+      slaveinfo#set_text (Printf.sprintf
+        "%d / <span foreground=\"#FF0000\">%d</span>" missing n_err)
+    else
+      slaveinfo#set_text (Printf.sprintf "%d / %d" missing n_err);
+    slaveinfo#set_use_markup true;
+    if errwin#misc#visible then update_errwin () in
   let callback () = on_current_term update; true in
   let _ = Glib.Timeout.add ~ms:300 ~callback in