Commit a2c5cb17 authored by MARCHE Claude's avatar MARCHE Claude

session stores the expanded/collapsed status of file and theories

parent 1753ab43
......@@ -18,42 +18,6 @@
(**************************************************************************)
(* TODO:
* when proof attempt is finished and is it the one currently selected,
the new output should be displayed on upper-right window
* when returning from edited proofs: should we run the prover again
immediately ?
* bug trouve par Johannes:
Pour reproduire le bug :
1) Partir d'un répértoire sans fichier de projet
2) Lancer why3db, ajouter un fichier
3) Prouver quelques buts (pas tous)
4) Choisir "Hide Proved Goals"
5) Prouver le reste des buts, la fênetre devient vide
6) Décocher "Hide Proved Goals"
Maintenant, le fichier réapparait dans la liste, mais on ne peut pas le
déplier, donc accéder au sous-buts, stats des appels de prouvers etc ...
Ce n'est pas un bug très grave, parce qu'il suffit de quitter l'ide,
puis le relancer, et là on peut de nouveau déplier le fichier.
* Francois :
- Les temps indiqués sont très bizarre, mais cela doit-être un bug
plus profond, au niveau de l'appel des prouveurs (wall time au lieu
de cpu time?)
- Si on modifie le fichier à droite, les buts ne sont pas marqués
obsolètes ou ajouté à gauche.
*)
open Format
let () =
......@@ -276,7 +240,6 @@ let (_ : GtkSignal.id) =
gconfig.tree_width <- w)
(* connecting to the Session model *)
(****************)
......@@ -356,6 +319,7 @@ let image_of_result ~obsolete result =
| Call_provers.HighFailure ->
if obsolete then !image_failure_obs else !image_failure
(* connecting to the Session model *)
module M = Session.Make
(struct
......@@ -388,7 +352,7 @@ module M = Session.Make
let set_row_status row b =
if b then
begin
goals_view#collapse_row row#path;
(* goals_view#collapse_row row#path; *)
goals_model#set ~row:row#iter ~column:status_column !image_yes;
end
else
......@@ -411,26 +375,56 @@ let set_proof_state ~obsolete a =
let model_index = Hashtbl.create 17
let get_any row =
let get_any_from_iter row =
try
let row = goals_model#get_iter row in
let idx = goals_model#get ~row ~column:index_column in
Hashtbl.find model_index idx
with Not_found -> invalid_arg "Gmain.get_index"
with Not_found -> invalid_arg "Gmain.get_any_from_iter"
let get_any (row:Gtk.tree_path) : M.any =
get_any_from_iter (goals_model#get_iter row)
let row_expanded b iter _path =
match get_any_from_iter iter with
| M.File f ->
eprintf "file_expanded <- %b@." b;
M.set_file_expanded f b
| M.Theory t ->
eprintf "theory_expanded <- %b@." b;
M.set_theory_expanded t b
| _ -> ()
let (_:GtkSignal.id) =
goals_view#connect#row_collapsed ~callback:(row_expanded false)
let (_:GtkSignal.id) =
goals_view#connect#row_expanded ~callback:(row_expanded true)
let notify any =
let row,exp =
match any with
| M.Goal g -> (M.goal_key g),false (* g.M.file_expanded *)
| M.Theory t -> (M.theory_key t),(M.theory_expanded t)
| M.File f -> f.M.file_key,f.M.file_expanded
| M.Proof_attempt a -> a.M.proof_key,false
| M.Transformation tr -> tr.M.transf_key,false
in
if exp then
(eprintf "exp@."; goals_view#expand_row row#path)
else
((*eprintf "col@.";*) goals_view#collapse_row row#path);
match any with
| M.Goal g ->
set_row_status (M.goal_key g) (M.goal_proved g)
set_row_status row (M.goal_proved g)
| M.Theory th ->
set_row_status (M.theory_key th) (M.verified th)
set_row_status row (M.verified th)
| M.File file ->
set_row_status file.M.file_key file.M.file_verified
set_row_status row file.M.file_verified
| M.Proof_attempt a ->
set_proof_state ~obsolete:a.M.proof_obsolete a
| M.Transformation tr ->
set_row_status tr.M.transf_key tr.M.transf_proved
set_row_status row tr.M.transf_proved
let init =
let cpt = ref (-1) in
fun row any ->
......@@ -445,6 +439,7 @@ let init =
begin
Hashtbl.replace model_index ind any;
end;
goals_view#expand_row row#path;
goals_model#set ~row:row#iter ~column:icon_column
(match any with
| M.Goal _ -> !image_file
......
......@@ -142,6 +142,7 @@ and goal =
mutable checksum : string;
goal_key : O.key;
mutable proved : bool;
mutable goal_expanded : bool;
external_proofs: (string, proof_attempt) Hashtbl.t;
transformations : (string, transf) Hashtbl.t;
}
......@@ -161,6 +162,7 @@ and theory =
theory_parent : file;
mutable goals : goal list;
mutable verified : bool;
mutable theory_expanded : bool;
}
and file =
......@@ -168,6 +170,7 @@ and file =
file_key : O.key;
mutable theories: theory list;
mutable file_verified : bool;
mutable file_expanded : bool;
}
type any =
......@@ -181,6 +184,9 @@ let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
let theory_expanded t = t.theory_expanded
let set_theory_expanded t b = t.theory_expanded <- b
let get_theory t =
match t.theory with
......@@ -211,6 +217,8 @@ let get_task g =
end
| Some t -> t
let set_file_expanded f b = f.file_expanded <- b
let all_files : file list ref = ref []
let get_all_files () = !all_files
......@@ -264,13 +272,13 @@ and save_trans fmt _ t =
fprintf fmt "@]@\n</transf>"
let save_theory fmt t =
fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\">"
t.theory_name t.verified;
fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\" expanded=\"%b\">"
t.theory_name t.verified t.theory_expanded;
List.iter (save_goal fmt) t.goals;
fprintf fmt "@]@\n</theory>"
let save_file fmt f =
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\">" f.file_name f.file_verified;
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\" expanded=\"%b\">" f.file_name f.file_verified f.file_expanded;
List.iter (save_theory fmt) f.theories;
fprintf fmt "@]@\n</file>"
......@@ -300,6 +308,8 @@ let check_file_verified f =
f.file_verified <- b;
!notify_fun (File f)
end
else
!notify_fun (File f)
let check_theory_proved t =
let b = List.for_all (fun g -> g.proved) t.goals in
......@@ -309,6 +319,9 @@ let check_theory_proved t =
!notify_fun (Theory t);
check_file_verified t.theory_parent
end
else
!notify_fun (Theory t)
let rec check_goal_proved g =
let b1 = Hashtbl.fold
......@@ -328,6 +341,8 @@ let rec check_goal_proved g =
| Parent_theory t -> check_theory_proved t
| Parent_transf t -> check_transf_proved t
end
else
!notify_fun (Goal g);
and check_transf_proved t =
let b = List.for_all (fun g -> g.proved) t.subgoals in
......@@ -611,6 +626,7 @@ let raw_add_goal parent name expl sum topt =
external_proofs = Hashtbl.create 7;
transformations = Hashtbl.create 3;
proved = false;
goal_expanded = false;
}
in
let any = Goal goal in
......@@ -638,7 +654,7 @@ let raw_add_transformation g trans =
!notify_fun any;
tr
let raw_add_theory mfile thopt thname =
let raw_add_theory mfile thopt thname exp =
let parent = mfile.file_key in
let key = O.create ~parent () in
let mth = { theory_name = thname;
......@@ -646,7 +662,9 @@ let raw_add_theory mfile thopt thname =
theory_key = key;
theory_parent = mfile;
goals = [] ;
verified = false }
verified = false;
theory_expanded = exp;
}
in
let any = Theory mth in
!init_fun key any;
......@@ -657,7 +675,7 @@ let raw_add_theory mfile thopt thname =
let add_theory mfile name th =
let tasks = List.rev (Task.split_theory th None None) in
let mth = raw_add_theory mfile (Some th) name in
let mth = raw_add_theory mfile (Some th) name true in
let goals =
List.fold_left
(fun acc t ->
......@@ -673,12 +691,14 @@ let add_theory mfile name th =
check_theory_proved mth;
mth
let raw_add_file f =
let raw_add_file f exp =
let key = O.create () in
let mfile = { file_name = f;
file_key = key;
theories = [] ;
file_verified = false }
file_verified = false;
file_expanded = exp;
}
in
all_files := !all_files @ [mfile];
let any = File mfile in
......@@ -709,7 +729,7 @@ let read_file fn =
let add_file f =
let theories = read_file f in
let mfile = raw_add_file f in
let mfile = raw_add_file f true in
let mths =
List.fold_left
(fun acc (_,name,t) ->
......@@ -718,7 +738,9 @@ let add_file f =
[] theories
in
mfile.theories <- List.rev mths;
check_file_verified mfile
check_file_verified mfile;
!notify_fun (File mfile)
let file_exists fn =
......@@ -737,7 +759,7 @@ let reload_proof ~provers obsolete goal pid old_a =
let p = Util.Mstr.find pid provers in
let old_res = old_a.proof_state in
let obsolete = obsolete or old_a.proof_obsolete in
eprintf "proof_obsolete : %b@." obsolete;
(* eprintf "proof_obsolete : %b@." obsolete; *)
let _a =
raw_add_external_proof ~obsolete ~edit:old_a.edited_as goal p old_res
in
......@@ -877,13 +899,13 @@ let reload_root_goal ~provers mth tname old_goals t : goal =
let reload_theory ~provers mfile old_theories (_,tname,th) =
eprintf "[Reload] theory '%s'@."tname;
let tasks = List.rev (Task.split_theory th None None) in
let mth = raw_add_theory mfile (Some th) tname in
let old_goals =
let old_goals, old_exp =
try
let old_mth = Util.Mstr.find tname old_theories in
old_mth.goals
with Not_found -> []
old_mth.goals, old_mth.theory_expanded
with Not_found -> [], true
in
let mth = raw_add_theory mfile (Some th) tname old_exp in
let goalsmap = List.fold_left
(fun goalsmap g -> Util.Mstr.add g.goal_name g goalsmap)
Util.Mstr.empty old_goals
......@@ -901,19 +923,7 @@ let reload_theory ~provers mfile old_theories (_,tname,th) =
(* reloads a file *)
let reload_file ~provers mf theories =
(*
eprintf "[Reload] file '%s'@." mf.file_name;
let theories =
try
read_file mf.file_name
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" mf.file_name
Exn_printer.exn_printer e;
(* TODO: do something clever than that! *)
exit 1
in
*)
let new_mf = raw_add_file mf.file_name in
let new_mf = raw_add_file mf.file_name mf.file_expanded in
let old_theories = List.fold_left
(fun acc t -> Util.Mstr.add t.theory_name t acc)
Util.Mstr.empty
......@@ -944,6 +954,14 @@ let reload_all provers =
(* session opening *)
(****************************)
let bool_attribute field r def =
try
match List.assoc field r.Xml.attributes with
| "true" -> true
| "false" -> false
| _ -> assert false
with Not_found -> def
let load_result r =
match r.Xml.name with
| "result" ->
......@@ -1060,7 +1078,8 @@ let load_theory ~env ~provers mf acc th =
try List.assoc "name" th.Xml.attributes
with Not_found -> assert false
in
let mth = raw_add_theory mf None thname in
let exp = bool_attribute "expanded" th true in
let mth = raw_add_theory mf None thname exp in
mth.goals <-
List.rev
(List.fold_left
......@@ -1078,7 +1097,8 @@ let load_file ~env ~provers f =
try List.assoc "name" f.Xml.attributes
with Not_found -> assert false
in
let mf = raw_add_file fn in
let exp = bool_attribute "expanded" f true in
let mf = raw_add_file fn exp in
mf.theories <-
List.rev
(List.fold_left (load_theory ~env ~provers mf) [] f.Xml.elements)
......
......@@ -126,14 +126,19 @@ module Make(O: OBSERVER) : sig
val theory_key : theory -> O.key
val verified : theory -> bool
val goals : theory -> goal list
val theory_expanded : theory -> bool
val set_theory_expanded : theory -> bool -> unit
type file = private
{ file_name : string;
file_key : O.key;
mutable theories: theory list;
mutable file_verified : bool;
mutable file_expanded : bool;
}
val set_file_expanded : file -> bool -> unit
type any =
| File of file
| Theory of theory
......
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