diff options
| -rw-r--r-- | ide/coqOps.ml | 8 | ||||
| -rw-r--r-- | ide/coqOps.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 133 |
3 files changed, 86 insertions, 57 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 8ba7c7019..af24d7f5f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -123,7 +123,7 @@ object method get_n_errors : int method get_errors : (int * string) list - method get_slaves_status : int * int + method get_slaves_status : int * int * string Int.Map.t method handle_failure : handle_exn_rty -> unit task @@ -151,6 +151,7 @@ object(self) (* proofs being processed by the slaves *) val mutable to_process = 0 val mutable processed = 0 + val mutable slaves_status = Int.Map.empty val feedbacks : feedback Queue.t = Queue.create () val feedback_timer = Ideutils.mktimer () @@ -357,6 +358,9 @@ object(self) | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n + | SlaveStatus(id,status), _ -> + log "SlaveStatus" None; + slaves_status <- Int.Map.add id status slaves_status | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" @@ -519,7 +523,7 @@ 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 get_slaves_status = processed, to_process, slaves_status method get_n_errors = Doc.fold_all document 0 (fun n _ _ s -> if has_flag s `ERROR then n+1 else n) diff --git a/ide/coqOps.mli b/ide/coqOps.mli index e313cd47a..cde6f3d00 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -24,7 +24,7 @@ object method get_n_errors : int method get_errors : (int * string) list - method get_slaves_status : int * int + method get_slaves_status : int * int * string Int.Map.t method handle_failure : Interface.handle_exn_rty -> unit task diff --git a/ide/coqide.ml b/ide/coqide.ml index 41e190002..f79322364 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1262,63 +1262,86 @@ let build_ui () = let () = slaveinfobut#misc#set_has_tooltip true in let () = slaveinfobut#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" ~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 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 -> ()) in let tip = GMisc.label ~text:"Double click to jump to error line" () in - let () = vb#pack ~expand:true frame#coerce 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 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 - 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 - (* So that the text is wrapped correctly in the model even if the window - * has never been shown *) - data#misc#realize (); - obj, (let last_update = ref (0,[]) in - fun tabno l -> - if !last_update = (tabno,l) then () + let add_page text w = + nb#append_page ~tab_label:(GMisc.label ~text ())#coerce w#coerce in + let _ = add_page "Errors" vb in + let _ = add_page "Workers" table_jobs 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,l; - store#clear (); - List.iter (fun (lno, msg) -> + 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 column1 lno; - store#set line column2 msg; - store#set line column3 tabno) l + 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 @@ -1326,10 +1349,12 @@ let build_ui () = ~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 + 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 = sn.coqops#get_slaves_status in + let processed, to_process, jobs = sn.coqops#get_slaves_status in let missing = to_process - processed in let n_err = sn.coqops#get_n_errors in if n_err > 0 then |