Commit 57309840 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fixed clean button

parent 640402ce
......@@ -450,8 +450,10 @@ module Model = struct
and transf =
{ parent_goal : goal;
transf_name : string;
mutable transf_proved : bool;
(*
transf : Task.task Trans.trans;
*)
transf_row : Gtk.tree_iter;
transf_db : Db.transf;
mutable subgoals : goal list;
......@@ -963,7 +965,6 @@ module Helpers = struct
let parent = g.Model.goal_row in
let row = goals_model#append ~parent () in
let tr = { Model.parent_goal = g;
Model.transf_name = tr_name;
Model.transf_proved = false;
Model.transf_row = row;
Model.transf_db = db_transf;
......@@ -2234,36 +2235,19 @@ let () =
let remove_proof_attempt a =
Db.remove_proof_attempt a.Model.proof_db;
let (_:bool) = goals_model#remove a.Model.proof_row in
()
let rec remove_transf t =
List.iter remove_subgoal t.Model.subgoals;
Db.remove_transformation t.Model.transf_db;
let (_:bool) = goals_model#remove t.Model.transf_row in
()
and remove_subgoal g =
Hashtbl.iter (fun _ a -> remove_proof_attempt a) g.Model.external_proofs;
Hashtbl.iter (fun _ t -> remove_transf t) g.Model.transformations;
Db.remove_subgoal g.Model.goal_db;
let (_:bool) = goals_model#remove g.Model.goal_row in
()
let remove_proof_attempt_and_check a =
remove_proof_attempt a;
let g = a.Model.proof_goal in
Hashtbl.remove g.Model.external_proofs a.Model.prover.prover_id;
Helpers.check_goal_proved g
let remove_transf_and_check t =
remove_transf t;
let remove_transf t =
(* TODO: remove subgoals first !!! *)
Db.remove_transformation t.Model.transf_db;
let (_:bool) = goals_model#remove t.Model.transf_row in
let g = t.Model.parent_goal in
Hashtbl.remove g.Model.transformations t.Model.transf_name;
Hashtbl.remove g.Model.transformations "split" (* hack !! *);
Helpers.check_goal_proved g
let confirm_remove_row r =
let row = filter_model#get_iter r in
match filter_model#get ~row ~column:Model.index_column with
......@@ -2275,12 +2259,12 @@ let confirm_remove_row r =
info_window `ERROR "Cannot remove a file"
| Model.Row_proof_attempt a ->
info_window
~callback:(fun () -> remove_proof_attempt_and_check a)
~callback:(fun () -> remove_proof_attempt a)
`QUESTION
"Do you really want to remove the selected proof attempt?"
| Model.Row_transformation tr ->
info_window
~callback:(fun () -> remove_transf_and_check tr)
~callback:(fun () -> remove_transf tr)
`QUESTION
"Do you really want to remove the selected transformation
and all its subgoals?"
......@@ -2304,22 +2288,16 @@ let () =
let rec clean_goal g =
if g.Model.proved then
begin
let l = Hashtbl.fold
(fun key a acc ->
Hashtbl.iter
(fun _ a ->
if a.Model.proof_obsolete || not (proof_successful a) then
(remove_proof_attempt a; key::acc)
else acc)
g.Model.external_proofs
[]
in List.iter (Hashtbl.remove g.Model.external_proofs) l;
let l = Hashtbl.fold
(fun key t acc ->
remove_proof_attempt a)
g.Model.external_proofs;
Hashtbl.iter
(fun _ t ->
if not t.Model.transf_proved then
(remove_transf t; key::acc)
else acc)
remove_transf t)
g.Model.transformations
[]
in List.iter (Hashtbl.remove g.Model.transformations) l;
end
else
Hashtbl.iter
......
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