Commit 81ec7577 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Improved display of tasks and transformations

parent 84f37510
......@@ -1693,7 +1693,8 @@ src/ide/why3_js.byte: $(TRYWHY3CMO) src/ide/why3_js.cmo
src/ide/why3_js.js: src/ide/why3_js.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
new_src_ide: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
......
......@@ -551,16 +551,16 @@ let interpNotif (n: notification) =
| Message m ->
begin
match m with
| Proof_error (nid, s) ->
| Proof_error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Proof error on selected node: \"%s\"" s)
| Transf_error (nid, s) ->
| Transf_error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Transformation error on selected node: \"%s\"" s)
| Strat_error (nid, s) ->
| Strat_error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Strategy error on selected node: \"%s\"" s)
| Query_Error (nid, s) ->
| Query_Error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Query error on selected node: \"%s\"" s)
| Query_Info (nid, s) -> PE.error_print_msg s
......
......@@ -297,17 +297,26 @@ let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let node_id_column = cols#add Gobject.Data.int
let status_column = cols#add Gobject.Data.gobject
let time_column = cols#add Gobject.Data.string
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let view_name_column = GTree.view_column ~title:"Theories/Goals" ()
let () =
view_name_column#pack name_renderer;
view_name_column#add_attribute name_renderer "text" name_column;
view_name_column#set_sizing `AUTOSIZE
(* view_name_column#set_sizing `AUTOSIZE; *)
view_name_column#set_resizable true;
view_name_column#set_max_width 500
let status_renderer = GTree.cell_renderer_pixbuf [ ]
let view_status_column = GTree.view_column ~title:"Status"
~renderer:(status_renderer, ["pixbuf", status_column])()
~renderer:(status_renderer, ["pixbuf", status_column])
()
let view_time_column =
let renderer = GTree.cell_renderer_text [`XALIGN 0.] in
GTree.view_column ~title:"Time"
~renderer:(renderer, ["text", time_column]) ()
let goals_model,goals_view =
Debug.dprintf debug "[GUI] Creating tree model...@?";
......@@ -319,11 +328,12 @@ let goals_model,goals_view =
*)
ignore (view#append_column view_name_column);
ignore (view#append_column view_status_column);
(*
ignore (view#append_column view_status_column);
ignore (view#append_column view_time_column);
*)
Debug.dprintf debug " done@.";
view_status_column#set_resizable false;
view_status_column#set_visible true;
view_time_column#set_resizable false;
view_time_column#set_visible true;
Debug.dprintf debug "[GTK IDE] done@.";
model,view
......@@ -826,7 +836,7 @@ let on_selected_row r =
task_view#source_buffer#set_text ""
else
send_request (Get_task id)
| _ -> task_view#source_buffer#set_text ""
| _ -> send_request (Get_task id)
with
| Not_found -> task_view#source_buffer#set_text ""
......@@ -1013,10 +1023,7 @@ let if_selected_alone id f =
| _ -> ()
let treat_notification n =
(* temporary: this should be better executed each time
one clicks on the tree view *)
command_entry#misc#grab_focus ();
match n with
begin match n with
| Node_change (id, uinfo) ->
begin
match uinfo with
......@@ -1079,6 +1086,11 @@ let treat_notification n =
end
| Dead _ ->
print_message "Serveur sent an unexpected notification '%a'. Please report." print_notify n
end;
(* temporary: this should be better executed each time
one clicks on the tree view *)
(* command_entry#misc#grab_focus () *)
()
(***********************)
......
......@@ -459,7 +459,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| ATh th ->
(theory_name th).Ident.id_string
| ATn tn ->
get_transf_name d.cont.controller_session tn
let name = get_transf_name d.cont.controller_session tn in
let args = get_transf_args d.cont.controller_session tn in
let full = String.concat " " (name :: args) in
if String.length full >= 40 then
String.sub full 0 40 ^ " ..."
else full
| APn pn ->
(get_proof_name d.cont.controller_session pn).Ident.id_string
| APa pa ->
......@@ -692,15 +697,19 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| ATh t ->
P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string))
| APa pid ->
let parid = get_proof_attempt_parent d.cont.controller_session pid in
let pa = get_proof_attempt_node d.cont.controller_session pid in
let parid = pa.parent in
let name = Pp.string_of Whyconf.print_prover pa.prover in
let s = task_of_id d parid in
P.notify (Task (nid,s))
P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n"))
| AFile f ->
P.notify (Task (nid, "File " ^ f.file_name))
| ATn tid ->
let name = get_transf_name d.cont.controller_session tid in
let args = get_transf_args d.cont.controller_session tid in
P.notify (Task (nid, "Transformation " ^ String.concat " " (name :: args)))
let parid = get_trans_parent d.cont.controller_session tid in
let s = task_of_id d parid in
P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n"))
(* -------------------- *)
......
......@@ -1361,7 +1361,9 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
(************************)
module Mprover = Whyconf.Mprover
(* dead code
module Sprover = Whyconf.Sprover
*)
module PHprover = Whyconf.Hprover
open Format
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment