Move error and job display to the lower right pane.

3 files changed, 142 insertions, 110 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f21027277..d53d288d7d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1253,114 +1253,11 @@ let build_ui () =
   let _ = Glib.Timeout.add ~ms:300 ~callback 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
+  let () = lower_hbox#pack slaveinfo#coerce in
+  let () = slaveinfo#misc#set_has_tooltip true in
+  let () = slaveinfo#misc#set_tooltip_markup
     "Proofs to be checked / Errors" in
-  let int_assoc s l =
-    match List.assoc s l with `IntC c -> c | _ -> assert false in
-  let string_assoc s l =
-    match List.assoc s l with `StringC c -> c | _ -> assert false in
-  let make_table_widget cd cb =
-    let frame = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in
-    let columns, store =
-      let cols = new GTree.column_list in
-      let columns = List.map (function
-        | (`Int,n,_)    -> n, `IntC (cols#add Gobject.Data.int)
-        | (`String,n,_) -> n, `StringC (cols#add Gobject.Data.string))
-      cd in
-      columns, 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 mk_rend c = GTree.cell_renderer_text [], ["text",c] in
-    let cols =
-      List.map2 (fun (_,c) (_,n,v) ->
-        let c = match c with
-          | `IntC c -> GTree.view_column ~renderer:(mk_rend c) ()
-          | `StringC c -> GTree.view_column ~renderer:(mk_rend c) () in
-        c#set_title n;
-        c#set_visible v;
-        c#set_sizing `AUTOSIZE;
-        c)
-      columns cd in
-    List.iter (fun c -> ignore(data#append_column c)) cols;
-    ignore(
-      data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
-    );
-    frame, (fun f -> f columns store) in
-  let errwin, fill_errwin =
-    let obj = GWindow.window ~title:"Errors & Workers status" ~deletable:true
-      ~position:`CENTER_ON_PARENT ~show:false ~width:500 ~height:400 () in
-    let table_errs, access_errs =
-      make_table_widget
-        [`Int,"Line",true; `String,"Error message",true; `Int,"Tab no",false]
-        (fun columns store tp vc ->
-          let row = store#get_iter tp in
-          let lno = store#get ~row ~column:(int_assoc "Line" columns) in
-          let tabno = store#get ~row ~column:(int_assoc "Tab no" columns) in
-          let sn = notebook#get_nth_term tabno in
-          let where = sn.script#buffer#get_iter (`LINE (lno-1)) in
-          sn.buffer#place_cursor ~where;
-          ignore(sn.script#scroll_to_iter
-            ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
-    let table_jobs, access_jobs =
-      make_table_widget
-        [`Int,"Worker",true; `String,"Job name",true; `Int,"Tab no",false]
-        (fun columns store tp vc -> 
-          let row = store#get_iter tp in
-          let w = store#get ~row ~column:(int_assoc "Worker" columns) in
-          let tabno = store#get ~row ~column:(int_assoc "Tab no" columns) in
-          let sn = notebook#get_nth_term tabno in
-          send_to_coq_aux (fun sn -> sn.coqops#stop_worker w) sn
-        ) in
-    let tip = GMisc.label ~text:"Double click to jump to error line" () in
-    let nb = GPack.notebook ~packing:obj#add () in
-    let vb = GPack.vbox ~homogeneous:false () in
-    let () = vb#pack ~expand:true table_errs#coerce in
-    let () = vb#pack ~expand:false ~padding:2 tip#coerce in
-    let add_page text w =
-      nb#append_page ~tab_label:(GMisc.label ~text ())#coerce w#coerce in
-    let _ = add_page "Errors" vb in
-    let vb = GPack.vbox ~homogeneous:false () in
-    let tip = GMisc.label ~text:"Double click to interrupt worker" () in
-    let () = vb#pack ~expand:true table_jobs#coerce in
-    let () = vb#pack ~expand:false ~padding:2 tip#coerce in
-    let _ = add_page "Workers" vb in
-    obj, (let last_update = ref (0,[],Int.Map.empty) in
-          fun tabno errs jobs ->
-            if !last_update = (tabno,errs,jobs) then ()
-            else begin
-              last_update := tabno,errs,jobs;
-              access_errs (fun _ store -> store#clear ());
-              List.iter (fun (lno, msg) -> access_errs (fun columns store ->
-                let line = store#append () in
-                store#set line (int_assoc "Line" columns) lno;
-                store#set line (string_assoc "Error message" columns) msg;
-                store#set line (int_assoc "Tab no" columns) tabno))
-              errs;
-              access_jobs (fun _ store -> store#clear ());
-              Int.Map.iter (fun id job -> access_jobs (fun columns store ->
-                let line = store#append () in
-                store#set line (int_assoc "Worker" columns) id;
-                store#set line (string_assoc "Job name" columns) job))
-              jobs;
-            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
-        (Util.pi3 sn.coqops#get_slaves_status)) in
-  let _ = slaveinfobut#connect#clicked ~callback:errwin#present in
   let update sn =
     let processed, to_process, jobs = sn.coqops#get_slaves_status in
     let missing = to_process - processed in
@@ -1371,7 +1268,8 @@ let build_ui () =
     else
       slaveinfo#set_text (Printf.sprintf "%d / %d" missing n_err);
     slaveinfo#set_use_markup true;
-    if errwin#misc#visible then update_errwin () in
+    sn.errpage#update sn.coqops#get_errors;
+    sn.jobpage#update (Util.pi3 sn.coqops#get_slaves_status) in
   let callback () = on_current_term update; true in
   let _ = Glib.Timeout.add ~ms:300 ~callback in
 
diff --git a/ide/session.ml b/ide/session.ml
index fe15ebb4bb..ae9bef9467 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -13,6 +13,18 @@ let prefs = Preferences.current
 (** A session is a script buffer + proof + messages,
     interacting with a coqtop, and a few other elements around *)
 
+class type errpage =
+  object
+    inherit GObj.widget
+    method update : (int * string) list -> unit
+  end
+
+class type jobpage =
+  object
+    inherit GObj.widget
+    method update : string Int.Map.t -> unit
+  end
+
 type session = {
   buffer : GText.buffer;
   script : Wg_ScriptView.script_view;
@@ -24,6 +36,8 @@ type session = {
   command : Wg_Command.command_window;
   finder : Wg_Find.finder;
   tab_label : GMisc.label;
+  errpage : errpage;
+  jobpage : jobpage;
 }
 
 let create_buffer () =
@@ -211,6 +225,104 @@ let set_buffer_handlers
   let _ = buffer#connect#after#mark_deleted ~callback:mark_deleted_cb in
   ()
 
+let find_int_col s l =
+  match List.assoc s l with `IntC c -> c | _ -> assert false
+
+let find_string_col s l =
+  match List.assoc s l with `StringC c -> c | _ -> assert false
+
+let make_table_widget cd cb =
+  let frame = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in
+  let columns, store =
+    let cols = new GTree.column_list in
+    let columns = List.map (function
+      | (`Int,n,_)    -> n, `IntC (cols#add Gobject.Data.int)
+      | (`String,n,_) -> n, `StringC (cols#add Gobject.Data.string))
+    cd in
+    columns, 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 mk_rend c = GTree.cell_renderer_text [], ["text",c] in
+  let cols =
+    List.map2 (fun (_,c) (_,n,v) ->
+      let c = match c with
+        | `IntC c -> GTree.view_column ~renderer:(mk_rend c) ()
+        | `StringC c -> GTree.view_column ~renderer:(mk_rend c) () in
+      c#set_title n;
+      c#set_visible v;
+      c#set_sizing `AUTOSIZE;
+      c)
+    columns cd in
+  List.iter (fun c -> ignore(data#append_column c)) cols;
+  ignore(
+    data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
+  );
+  frame, (fun f -> f columns store)
+
+let create_errpage (script : Wg_ScriptView.script_view) : errpage =
+  let table, access =
+    make_table_widget
+      [`Int,"Line",true; `String,"Error message",true]
+      (fun columns store tp vc ->
+        let row = store#get_iter tp in
+        let lno = store#get ~row ~column:(find_int_col "Line" columns) in
+        let where = script#buffer#get_iter (`LINE (lno-1)) in
+        script#buffer#place_cursor ~where;
+        ignore (script#scroll_to_iter
+		  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
+  let tip = GMisc.label ~text:"Double click to jump to error line" () in
+  let box = GPack.vbox ~homogeneous:false () in
+  let () = box#pack ~expand:true table#coerce in
+  let () = box#pack ~expand:false ~padding:2 tip#coerce in
+  let last_update = ref [] in
+  object (self)
+    inherit GObj.widget box#as_widget
+    method update errs =
+      if !last_update = errs then ()
+      else begin
+	last_update := errs;
+	access (fun _ store -> store#clear ());
+	List.iter (fun (lno, msg) -> access (fun columns store ->
+          let line = store#append () in
+          store#set line (find_int_col "Line" columns) lno;
+          store#set line (find_string_col "Error message" columns) msg))
+          errs
+      end
+  end
+
+let create_jobpage coqtop coqops : jobpage =
+  let table, access =
+    make_table_widget
+      [`Int,"Worker",true; `String,"Job name",true]
+      (fun columns store tp vc ->
+        let row = store#get_iter tp in
+        let w = store#get ~row ~column:(find_int_col "Worker" columns) in
+	let info () = Minilib.log ("Coq busy, discarding query") in
+	Coq.try_grab coqtop (coqops#stop_worker w) info
+      ) in
+  let tip = GMisc.label ~text:"Double click to interrupt worker" () in
+  let box = GPack.vbox ~homogeneous:false () in
+  let () = box#pack ~expand:true table#coerce in
+  let () = box#pack ~expand:false ~padding:2 tip#coerce in
+  let last_update = ref Int.Map.empty in
+  object (self)
+    inherit GObj.widget box#as_widget
+    method update jobs =
+      if !last_update = jobs then ()
+      else begin
+	last_update := jobs;
+	access (fun _ store -> store#clear ());
+	Int.Map.iter (fun id job -> access (fun columns store ->
+          let line = store#append () in
+          store#set line (find_int_col "Worker" columns) id;
+          store#set line (find_string_col "Job name" columns) job))
+          jobs
+      end
+  end
+
 let create_proof () =
   let proof = Wg_ProofView.proof_view () in
   let _ = proof#misc#set_can_focus true in
@@ -241,6 +353,8 @@ let create file coqtop_args =
   let _ = fops#update_stats in
   let cops =
     new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
+  let errpage = create_errpage script in
+  let jobpage = create_jobpage coqtop cops in
   let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
   let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in
   let _ = Coq.init_coqtop coqtop cops#initialize in
@@ -255,6 +369,8 @@ let create file coqtop_args =
     command=command;
     finder=finder;
     tab_label= GMisc.label ~text:basename ();
+    errpage=errpage;
+    jobpage=jobpage
   }
 
 let kill (sn:session) =
@@ -282,8 +398,10 @@ let build_layout (sn:session) =
     ~packing:state_paned#add1 () in
   let proof_scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in
-  let message_frame = GBin.frame ~shadow_type:`IN
-    ~packing:state_paned#add2 () in
+  let message_frame = GPack.notebook ~packing:state_paned#add () in
+  let add_msg_page text w =
+    ignore (message_frame#append_page
+	      ~tab_label:(GMisc.label ~text ())#coerce w#coerce) in
   let session_tab = GPack.hbox ~homogeneous:false () in
   let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
     ~packing:session_tab#pack () in
@@ -313,7 +431,9 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  message_frame#add sn.messages#coerce;
+  add_msg_page "Messages" sn.messages;
+  add_msg_page "Errors" sn.errpage;
+  add_msg_page "Jobs" sn.jobpage;
   session_tab#pack sn.tab_label#coerce;
   img#set_stock `YES;
   eval_paned#set_position 1;
diff --git a/ide/session.mli b/ide/session.mli
index e98cbbd7d9..737b6d10de 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -9,6 +9,18 @@
 (** A session is a script buffer + proof + messages,
     interacting with a coqtop, and a few other elements around *)
 
+class type errpage =
+  object
+    inherit GObj.widget
+    method update : (int * string) list -> unit
+  end
+
+class type jobpage =
+  object
+    inherit GObj.widget
+    method update : string Int.Map.t -> unit
+  end
+
 type session = {
   buffer : GText.buffer;
   script : Wg_ScriptView.script_view;
@@ -20,6 +32,8 @@ type session = {
   command : Wg_Command.command_window;
   finder : Wg_Find.finder;
   tab_label : GMisc.label;
+  errpage : errpage;
+  jobpage : jobpage;
 }
 
 (** [create filename coqtop_args] *)