Commit cd2443ec authored by MARCHE Claude's avatar MARCHE Claude

prover output is displayed immediately if row is selected

parent a94b1c6a
* marks an incompatible change
o fix BTS 12457
o fix BTS 13854
o fix BTS 13849
o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
......
......@@ -166,7 +166,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* fix bugs and update the BTS
- (JCF) reject global "val"s in typing environment for logic decls.
- (CLAUDE) Refreshing the IDE pane for prover output
- DONE (CLAUDE) Refreshing the IDE pane for prover output
* (CLAUDE) IDE:
- DONE enlarge font (menu + shortcut Ctrl-+)
......@@ -178,6 +178,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- syntax highlighting bugs ?
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
NEED FEEDBACK which ones ???
- DONE add a scrollbar for the left panel
* DONE (FRANCOIS) move Session module and its dependencies into the Why3 library
......
......@@ -476,7 +476,6 @@ let set_proof_state a =
let model_index = Hashtbl.create 17
let get_any_from_iter row =
try
let idx = goals_model#get ~row ~column:index_column in
......@@ -515,6 +514,54 @@ let (_:GtkSignal.id) =
goals_view#connect#row_expanded ~callback:(row_expanded true)
let session_needs_saving = ref false
let current_selected_row = ref None
let current_env_session = ref None
let env_session () =
match !current_env_session with
| None -> assert false
| Some e -> e
let display_task t =
let task_text = Pp.string_of Pretty.print_task t in
task_view#source_buffer#set_text task_text;
task_view#scroll_to_mark `INSERT
let split_transformation = "split_goal"
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"
let update_task_view a =
match a with
| S.Goal g ->
if (Gconfig.config ()).intro_premises then
let trans =
Trans.lookup_transform intro_transformation (env_session()).S.env
in
display_task (Trans.apply trans (S.goal_task g))
else
display_task (S.goal_task g)
| S.Theory _th ->
task_view#source_buffer#set_text ""
| S.File _file ->
task_view#source_buffer#set_text ""
| S.Proof_attempt a ->
let o =
match a.S.proof_state with
| S.Undone S.Interrupted ->
"proof not yet scheduled for running"
| S.Undone S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button"
| S.Undone S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button"
| S.Done r -> r.Call_provers.pr_output
| S.Undone S.Scheduled-> "proof scheduled but not running yet"
| S.Undone S.Running -> "prover currently running"
| S.InternalFailure e ->
let b = Buffer.create 37 in
bprintf b "%a" Exn_printer.exn_printer e;
Buffer.contents b
in
task_view#source_buffer#set_text o
| S.Transf _tr ->
task_view#source_buffer#set_text ""
module M = Session_scheduler.Make
(struct
......@@ -552,6 +599,7 @@ module M = Session_scheduler.Make
(if r=0 then "Running: 0" else
"Running: " ^ (string_of_int r)^ " " ^ (fan (!c / 10)))
let notify any =
session_needs_saving := true;
let row,exp =
......@@ -563,6 +611,13 @@ let notify any =
| S.Proof_attempt a -> a.S.proof_key,false
| S.Transf tr -> tr.S.transf_key,tr.S.transf_expanded
in
let ind = goals_model#get ~row:row#iter ~column:index_column in
begin
match !current_selected_row with
| Some r when r == ind ->
update_task_view any
| _ -> ()
end;
if exp then goals_view#expand_to_path row#path else
goals_view#collapse_row row#path;
match any with
......@@ -688,20 +743,21 @@ let () =
exit 2;
end
let env_session,sched =
let sched =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
let session =
if Sys.file_exists project_dir then S.read_session project_dir
else S.create_session project_dir in
let env_session,(_:bool) =
let env,(_:bool) =
M.update_session ~allow_obsolete:true session gconfig.env
gconfig.Gconfig.config
in
let sched = M.init gconfig.max_running_processes in
dprintf debug "@]@\n[Info] Opening session: done@.";
session_needs_saving := false;
ref env_session, sched
current_env_session := Some env;
sched
with e ->
eprintf "@[Error while opening session:@ %a@.@]"
Exn_printer.exn_printer e;
......@@ -717,12 +773,12 @@ let () =
match file_to_read with
| None -> ()
| Some fn ->
if S.PHstr.mem !env_session.S.session.S.session_files fn then
if S.PHstr.mem (env_session()).S.session.S.session_files fn then
dprintf debug "[Info] file %s already in database@." fn
else
try
dprintf debug "[Info] adding file %s in database@." fn;
ignore (M.add_file !env_session fn)
ignore (M.add_file (env_session()) fn)
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn
Exn_printer.exn_printer e;
......@@ -741,7 +797,7 @@ let prover_on_selected_goals pr =
try
let a = get_any_from_row_reference row in
M.run_prover
!env_session sched
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~timelimit:gconfig.time_limit
pr a
......@@ -758,7 +814,7 @@ let replay_obsolete_proofs () =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
M.replay !env_session sched ~obsolete_only:true
M.replay (env_session()) sched ~obsolete_only:true
~context_unproved_goals_only:!context_unproved_goals_only a)
(get_selected_row_references ())
......@@ -788,16 +844,12 @@ let set_archive_proofs b () =
(* method: split selected goals *)
(*****************************************************)
let split_transformation = "split_goal"
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"
let apply_trans_on_selection tr =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
M.transform !env_session sched
M.transform (env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
tr
a)
......@@ -836,7 +888,7 @@ let select_file () =
let f = Sysutil.relativize_filename project_dir f in
eprintf "Adding file '%s'@." f;
try
ignore (M.add_file !env_session f)
ignore (M.add_file (env_session()) f)
with e ->
fprintf str_formatter
"@[Error while reading file@ '%s':@ %a@]" f
......@@ -891,7 +943,7 @@ let (_ : GMenu.image_menu_item) =
let save_session () =
if !session_needs_saving then begin
eprintf "[Info] saving session@.";
S.save_session !env_session.S.session;
S.save_session (env_session()).S.session;
session_needs_saving := false;
end
......@@ -1000,7 +1052,7 @@ let rec collapse_verified = function
| any -> S.iter collapse_verified any
let collapse_all_verified_things () =
S.session_iter collapse_verified !env_session.S.session
S.session_iter collapse_verified (env_session()).S.session
let (_ : GMenu.image_menu_item) =
view_factory#add_image_item ~key:GdkKeysyms._C
......@@ -1358,12 +1410,12 @@ let reload () =
(in order to reload the files which are "use") *)
gconfig.env <- Env.create_env loadpath;
(** reload the session *)
let old_session = (!env_session).S.session in
let old_session = (env_session()).S.session in
let new_env_session,(_:bool) =
M.update_session ~allow_obsolete:true old_session gconfig.env
gconfig.Gconfig.config
in
env_session := new_env_session
current_env_session := Some new_env_session
with
| e ->
let e = match e with
......@@ -1439,7 +1491,7 @@ let edit_selected_row r =
()
| S.Proof_attempt a ->
M.edit_proof
!env_session sched ~default_editor:gconfig.default_editor a
(env_session()) sched ~default_editor:gconfig.default_editor a
| S.Transf _ -> ()
let edit_current_proof () =
......@@ -1621,46 +1673,12 @@ let () =
(* Bind events *)
(***************)
let display_task t =
let task_text = Pp.string_of Pretty.print_task t in
task_view#source_buffer#set_text task_text;
task_view#scroll_to_mark `INSERT
let update_task_view a =
match a with
| S.Goal g ->
if (Gconfig.config ()).intro_premises then
let trans =
Trans.lookup_transform intro_transformation !env_session.S.env in
display_task (Trans.apply trans (S.goal_task g))
else
display_task (S.goal_task g)
| S.Theory _th ->
task_view#source_buffer#set_text ""
| S.File _file ->
task_view#source_buffer#set_text ""
| S.Proof_attempt a ->
let o =
match a.S.proof_state with
| S.Undone S.Interrupted ->
"proof not yet scheduled for running"
| S.Undone S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button"
| S.Undone S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button"
| S.Done r -> r.Call_provers.pr_output
| S.Undone S.Scheduled-> "proof scheduled but not running yet"
| S.Undone S.Running -> "prover currently running"
| S.InternalFailure e ->
let b = Buffer.create 37 in
bprintf b "%a" Exn_printer.exn_printer e;
Buffer.contents b
in
task_view#source_buffer#set_text o
| S.Transf _tr ->
task_view#source_buffer#set_text ""
(* to be run when a row in the tree view is selected *)
let select_row r =
let ind = goals_model#get ~row:r#iter ~column:index_column in
current_selected_row := Some ind;
let a = get_any_from_row_reference r in
update_task_view a;
match a 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