Commit 357481b9 authored by MARCHE Claude's avatar MARCHE Claude

GTK: added a GTK tree, display the task of the selected row

parent 9669f0c8
......@@ -2,6 +2,9 @@
open Format
open Why3
open Gconfig
open Stdlib
open Session_itp
open Controller_itp
let debug = Debug.lookup_flag "ide_info"
......@@ -40,6 +43,14 @@ let gconfig = try
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let task_driver =
let main = Whyconf.get_main gconfig.config in
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
Driver.load_driver gconfig.env d []
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers gconfig.config
......@@ -53,25 +64,9 @@ let () =
Gconfig.init ()
(************)
(* controller instance on the GTK scheduler *)
module S = struct
let idle ~prio f =
let (_ : GMain.Idle.id) = GMain.Idle.add ~prio f in ()
let timeout ~ms f =
let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
()
end
module C = Controller_itp.Make(S)
(***************)
(* Main window *)
(***************)
(**********************)
(* Graphical elements *)
(**********************)
let main_window =
let w = GWindow.window
......@@ -145,6 +140,13 @@ let scrollview =
gconfig.tree_width <- w)
in sv
let vbox222 = GPack.vbox ~packing:hp#add ()
(* the scrolled window 2.2.1 contains a GTK tree
*)
(* view for the session tree *)
let scrolled_session_view =
GBin.scrolled_window
......@@ -153,15 +155,31 @@ let scrolled_session_view =
~packing:scrollview#add
()
let session_view =
GText.view ~editable:false ~cursor_visible:false
~packing:scrolled_session_view#add ()
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let index_column = cols#add Gobject.Data.int
let display_session () =
let s = Pp.string_of Controller_itp.print_session cont in
session_view#buffer#set_text s
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
let vbox222 = GPack.vbox ~packing:hp#add ()
let goals_model,goals_view =
Debug.dprintf debug "[GUI] Creating tree model...@?";
let model = GTree.tree_store cols in
let view = GTree.view ~model ~packing:scrolled_session_view#add () in
(*
let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
let () = view#set_rules_hint true in
*)
ignore (view#append_column view_name_column);
(*
ignore (view#append_column view_status_column);
ignore (view#append_column view_time_column);
*)
Debug.dprintf debug " done@.";
model,view
(* vbox222 contains:
2.2.2.1 a view of the current task
......@@ -182,35 +200,113 @@ let task_view =
~packing:scrolled_task_view#add
()
(* TEMPORARY !!! *)
let first_goal () =
Session_itp.get_task cont.Controller_itp.controller_session (Obj.magic 0)
let command_entry = GEdit.entry ~packing:vbox222#add ()
let message_zone =
GText.view ~editable:false ~cursor_visible:false
~packing:vbox222#add ()
let clear_command_entry () = command_entry#set_text ""
let task_driver =
let main = Whyconf.get_main gconfig.config in
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
(********************************************)
(* controller instance on the GTK scheduler *)
(********************************************)
module S = struct
let idle ~prio f =
let (_ : GMain.Idle.id) = GMain.Idle.add ~prio f in ()
let timeout ~ms f =
let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
()
end
module C = Controller_itp.Make(S)
(***********************************)
(* Mapping session to the GTK tree *)
(***********************************)
type index =
| Inone
| IproofNode of proofNodeID
| Ifile of file
| Itheory of theory
let model_index : index Hint.t = Stdlib.Hint.create 17
let new_node =
let cpt = ref (-1) in
fun ?parent name ind ->
incr cpt;
Hint.add model_index !cpt ind;
let parent = Opt.map (fun x -> x#iter) parent in
let iter = goals_model#append ?parent () in
goals_model#set ~row:iter ~column:name_column name;
goals_model#set ~row:iter ~column:index_column !cpt;
goals_model#get_row_reference (goals_model#get_path iter)
let build_subtree_from_goal ses th_row_reference id =
let name = get_proof_name ses id in
let _row_ref =
new_node ~parent:th_row_reference name.Ident.id_string
(IproofNode id)
in
Driver.load_driver cont.Controller_itp.controller_env d []
(* TODO: continue to add transformations and subgoals as sub-trees *)
()
let build_tree_from_session ses =
let files = get_files ses in
Stdlib.Hstr.iter
(fun _ file ->
let file_row_reference = new_node file.file_name (Ifile file) in
List.iter (fun th ->
let th_row_reference =
new_node ~parent:file_row_reference
(theory_name th).Ident.id_string
(Itheory th)
in
List.iter (build_subtree_from_goal ses th_row_reference)
(theory_goals th))
file.file_theories)
files
(******************)
(* actions *)
(******************)
let current_selected_index = ref Inone
let run_strategy_on_task s =
match !current_selected_index with
| IproofNode id ->
let l = Session_user_interface.strategies
cont.controller_env gconfig.config
in
let st = List.filter (fun (_,c,_,_) -> c=s) l in
begin
match st with
| [(n,_,_,st)] ->
printf "running strategy '%s'@." n;
let callback sts =
printf "Strategy status: %a@." print_strategy_status sts
in
C.run_strategy_on_goal cont id st ~callback
| _ -> printf "Strategy '%s' not found@." s
end
| _ -> ()
let clear_command_entry () = command_entry#set_text ""
let interp cmd =
match cmd with
| "p" -> display_session (); clear_command_entry ()
| "g" -> clear_command_entry ();
let task = first_goal () in
let s = Pp.string_of
(Driver.print_task ~cntexample:false task_driver)
task
in task_view#source_buffer#set_text s
| "s" -> clear_command_entry ();
run_strategy_on_task "1"
| _ -> message_zone#buffer#set_text ("unknown command '"^cmd^"'")
let (_ : GtkSignal.id) =
......@@ -218,9 +314,42 @@ let (_ : GtkSignal.id) =
~callback:(fun () -> interp command_entry#text)
let get_selected_row_references () =
List.map
(fun path -> goals_model#get_row_reference path)
goals_view#selection#get_selected_rows
let on_selected_row r =
let index = goals_model#get ~row:r#iter ~column:index_column in
try
let index = Hint.find model_index index in
current_selected_index := index;
match index with
| IproofNode id ->
let task = get_task cont.controller_session id in
let s = Pp.string_of
(Driver.print_task ~cntexample:false task_driver)
task
in task_view#source_buffer#set_text s
| _ -> task_view#source_buffer#set_text ""
with
| Not_found -> task_view#source_buffer#set_text ""
let (_ : GtkSignal.id) =
goals_view#selection#connect#after#changed ~callback:
(fun () ->
match get_selected_row_references () with
| [r] -> on_selected_row r
| _ -> ())
(***********************)
(* start the interface *)
(***********************)
let () =
build_tree_from_session cont.controller_session;
(* temporary *)
goals_view#expand_all ();
main_window#add_accel_group accel_group;
main_window#set_icon (Some !Gconfig.why_icon);
main_window#show ();
......
open Format
(* TODO: raise exceptions instead of using explicit eprintf/exit *)
let cont_from_files spec usage_str env files provers =
if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
let fname = Queue.peek files in
(* extract project directory, and create it if needed *)
let dir =
if Filename.check_suffix fname ".why" ||
Filename.check_suffix fname ".mlw"
then Filename.chop_extension fname
else let _ = Queue.pop files in fname
in
if Sys.file_exists dir then
begin
if not (Sys.is_directory dir) then
begin
Format.eprintf
"[Error] @[When@ more@ than@ one@ file@ is@ given@ on@ the@ \
command@ line@ the@ first@ one@ must@ be@ the@ directory@ \
of@ the@ session.@]@.";
Arg.usage spec usage_str; exit 1
end
end
else
begin
eprintf "[GUI] '%s' does not exist. \
Creating directory of that name for the project@." dir;
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = Session_itp.load_session dir in
eprintf "using shapes: %a@." pp_print_bool use_shapes;
(* create the controller *)
let c = Controller_itp.create_controller env ses in
(* update the session *)
Controller_itp.reload_files c env ~use_shapes;
(* add files to controller *)
Queue.iter (fun fname -> Controller_itp.add_file c fname) files;
(* load provers drivers *)
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver env p.Whyconf.driver [] in
Whyconf.Hprover.add c.Controller_itp.controller_provers p.Whyconf.prover (p,d)
with e ->
let p = p.Whyconf.prover in
eprintf "Failed to load driver for %s %s: %a@."
p.Whyconf.prover_name p.Whyconf.prover_version
Exn_printer.exn_printer e)
provers;
(* return the controller *)
c
(***************** strategies *****************)
let loaded_strategies = ref []
let strategies env config =
match !loaded_strategies with
| [] ->
let strategies = Whyconf.get_strategies config in
let strategies =
Stdlib.Mstr.fold_left
(fun acc _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse2 env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Format.eprintf "[Why3shell] Strategy '%s' loaded.@." name;
(name, shortcut, st.Whyconf.strategy_desc, code) :: acc
with Strategy_parser.SyntaxError msg ->
Format.eprintf
"[Why3shell warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
let strategies = List.rev strategies in
loaded_strategies := strategies;
strategies
| l -> l
......@@ -526,38 +526,10 @@ let test_transform_and_display fmt args =
| _ -> printf "Error: Give the name of the transformation@."
(***************** strategy *****************)
let loaded_strategies = ref []
let strategies () =
match !loaded_strategies with
| [] ->
let strategies = Whyconf.get_strategies config in
let strategies =
Stdlib.Mstr.fold_left
(fun acc _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse2 env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Format.eprintf "[Why3shell] Strategy '%s' loaded.@." name;
(name, shortcut, st.Whyconf.strategy_desc, code) :: acc
with Strategy_parser.SyntaxError msg ->
Format.eprintf
"[Why3shell warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
let strategies = List.rev strategies in
loaded_strategies := strategies;
strategies
| l -> l
let list_strategies _fmt _args =
let l = strategies () in
let l = Session_user_interface.strategies
cont.Controller_itp.controller_env config
in
let pp_strat fmt (n,s,desc,_) = fprintf fmt "%s (%s): %s" s n desc in
printf "@[<hov 2>== Known strategies ==@\n%a@]@."
(Pp.print_list Pp.newline pp_strat) l
......@@ -565,7 +537,9 @@ let list_strategies _fmt _args =
let run_strategy _fmt args =
match args with
| [s] ->
let l = strategies () in
let l = Session_user_interface.strategies
cont.Controller_itp.controller_env config
in
let st = List.filter (fun (_,c,_,_) -> c=s) l in
begin
match st with
......
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