Commit fd81ec38 authored by MARCHE Claude's avatar MARCHE Claude

new IDE: removing and cleaning reimplemented

parent 277ca2d3
......@@ -1025,7 +1025,8 @@ endif
MODULESTODOC = util/util util/hashweak \
core/ident core/ty core/term core/decl core/theory \
core/env core/task \
driver/whyconf driver/driver
driver/whyconf driver/driver \
ide/session
# transform/introduction \
# ide/db
......
......@@ -1250,25 +1250,22 @@ let () =
(* removing *)
(*************)
(*
let confirm_remove_row r =
let row = goals_model#get_iter r in
match goals_model#get ~row ~column:M.index_column with
| M.Row_goal _g ->
match get_any r with
| M.Goal _g ->
info_window `ERROR "Cannot remove a goal"
| M.Row_theory _th ->
| M.Theory _th ->
info_window `ERROR "Cannot remove a theory"
| M.Row_file _file ->
| M.File _file ->
info_window `ERROR "Cannot remove a file"
| M.Row_proof_attempt a ->
| M.Proof_attempt a ->
info_window
~callback:(fun () -> remove_proof_attempt a)
~callback:(fun () -> M.remove_proof_attempt a)
`QUESTION
"Do you really want to remove the selected proof attempt?"
| M.Row_transformation tr ->
| M.Transformation tr ->
info_window
~callback:(fun () -> remove_transf tr)
~callback:(fun () -> M.remove_transformation tr)
`QUESTION
"Do you really want to remove the selected transformation
and all its subgoals?"
......@@ -1280,6 +1277,7 @@ let confirm_remove_selection () =
| _ ->
info_window `INFO "Please select exactly one item to remove"
let () =
let b = GButton.button ~packing:cleaning_box#add ~label:"Remove" () in
b#misc#set_tooltip_markup "Removes the selected\n<b>proof</b> or <b>transformation</b>";
......@@ -1289,44 +1287,9 @@ let () =
b#connect#pressed ~callback:confirm_remove_selection
in ()
let rec clean_goal g =
if g.M.proved then
begin
Hashtbl.iter
(fun _ a ->
if a.M.proof_obsolete || not (proof_successful a) then
remove_proof_attempt a)
g.M.external_proofs;
Hashtbl.iter
(fun _ t ->
if not t.M.transf_proved then
remove_transf t)
g.M.transformations
end
else
Hashtbl.iter
(fun _ t -> List.iter clean_goal t.M.subgoals)
g.M.transformations
let clean_row r =
let row = goals_model#get_iter r in
match goals_model#get ~row ~column:M.index_column with
| M.Row_goal g -> clean_goal g
| M.Row_theory th ->
List.iter clean_goal th.M.goals
| M.Row_file file ->
List.iter
(fun th ->
List.iter clean_goal th.M.goals)
file.M.theories
| M.Row_proof_attempt a ->
clean_goal a.M.proof_goal
| M.Row_transformation tr ->
List.iter clean_goal tr.M.subgoals
let clean_selection () =
List.iter clean_row goals_view#selection#get_selected_rows
List.iter (fun r -> M.clean (get_any r))
goals_view#selection#get_selected_rows
let () =
let b = GButton.button ~packing:cleaning_box#add ~label:"Clean" () in
......@@ -1337,7 +1300,6 @@ let () =
b#connect#pressed ~callback:clean_selection
in ()
*)
(***************)
(* Bind events *)
......
......@@ -1441,52 +1441,17 @@ let edit_proof ~default_editor ~project_dir a =
(* removing *)
(*************)
(*
let remove_proof_attempt a =
Db.remove_proof_attempt a.proof_db;
let (_:bool) = goals_model#remove a.proof_row in
O.remove a.proof_key;
let g = a.proof_goal in
Hashtbl.remove g.external_proofs a.prover.prover_id;
Helpers.check_goal_proved g
check_goal_proved g
let remove_transf t =
(* TODO: remove subgoals first !!! *)
Db.remove_transformation t.transf_db;
let (_:bool) = goals_model#remove t.transf_row in
let remove_transformation t =
O.remove t.transf_key;
let g = t.parent_goal in
Hashtbl.remove g.transformations "split" (* hack !! *);
Helpers.check_goal_proved g
let confirm_remove_row r =
let row = goals_model#get_iter r in
match goals_model#get ~row ~column:index_column with
| Row_goal _g ->
info_window `ERROR "Cannot remove a goal"
| Row_theory _th ->
info_window `ERROR "Cannot remove a theory"
| Row_file _file ->
info_window `ERROR "Cannot remove a file"
| Row_proof_attempt a ->
info_window
~callback:(fun () -> remove_proof_attempt a)
`QUESTION
"Do you really want to remove the selected proof attempt?"
| Row_transformation tr ->
info_window
~callback:(fun () -> remove_transf tr)
`QUESTION
"Do you really want to remove the selected transformation
and all its subgoals?"
let confirm_remove_selection () =
match goals_view#selection#get_selected_rows with
| [] -> ()
| [r] -> confirm_remove_row r
| _ ->
info_window `INFO "Please select exactly one item to remove"
Hashtbl.remove g.transformations t.transf.transformation_name;
check_goal_proved g
let rec clean_goal g =
if g.proved then
......@@ -1499,7 +1464,7 @@ let rec clean_goal g =
Hashtbl.iter
(fun _ t ->
if not t.transf_proved then
remove_transf t)
remove_transformation t)
g.transformations
end
else
......@@ -1508,25 +1473,20 @@ let rec clean_goal g =
g.transformations
let clean_row r =
let row = goals_model#get_iter r in
match goals_model#get ~row ~column:index_column with
| Row_goal g -> clean_goal g
| Row_theory th ->
List.iter clean_goal th.goals
| Row_file file ->
let clean a =
match a with
| Goal g -> clean_goal g
| Theory th -> List.iter clean_goal th.goals
| File file ->
List.iter
(fun th ->
List.iter clean_goal th.goals)
file.theories
| Row_proof_attempt a ->
| Proof_attempt a ->
clean_goal a.proof_goal
| Row_transformation tr ->
| Transformation tr ->
List.iter clean_goal tr.subgoals
*)
end
(*
......
......@@ -17,10 +17,12 @@
(* *)
(**************************************************************************)
(** Proof sessions *)
open Why
(** {Prover's data} *)
(** {2 Prover's data} *)
type prover_data = private
{ prover_id : string;
prover_name : string;
......@@ -32,13 +34,14 @@ type prover_data = private
}
(** record of necessary data for a given external prover *)
val get_prover_data :
val get_prover_data :
Env.env -> Util.Mstr.key -> Whyconf.config_prover ->
prover_data Util.Mstr.t -> prover_data Util.Mstr.t
(** loads all provers from the current configuration *)
(** {Transformation's data} *)
type transformation_data
(** {2 Transformation's data} *)
type transformation_data
(** record data for transformations *)
val transformation_id : transformation_data -> string
......@@ -47,7 +50,8 @@ val transformation_id : transformation_data -> string
val lookup_transformation : Env.env -> string -> transformation_data
(** returns a transformation from its Why3 name *)
(** {Proof attempts} *)
(** {2 Proof attempts} *)
type proof_attempt_status = private
| Undone
| Scheduled (** external proof attempt is scheduled *)
......@@ -55,7 +59,8 @@ type proof_attempt_status = private
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
(** {Observers signature} *)
(** {2 Observers signature} *)
module type OBSERVER = sig
type key
......@@ -84,10 +89,11 @@ module type OBSERVER = sig
end
(** {Main functor} *)
(** {2 Main functor} *)
module Make(O: OBSERVER) : sig
(** {static state of a session} *)
(** {2 static state of a session} *)
type goal
(** a goal *)
......@@ -125,7 +131,7 @@ module Make(O: OBSERVER) : sig
val external_proofs : goal -> (string, proof_attempt) Hashtbl.t
type theory
type theory
(** a theory, holding a collection of goals *)
val theory_name : theory -> string
......@@ -154,19 +160,15 @@ module Make(O: OBSERVER) : sig
| Transformation of transf
(*****************************)
(* *)
(* save/load state *)
(* *)
(*****************************)
(** {2 Save and load a state} *)
val open_session :
val open_session :
env:Env.env ->
provers:prover_data Util.Mstr.t ->
init:(O.key -> any -> unit) ->
notify:(any -> unit) ->
notify:(any -> unit) ->
string -> unit
(** starts a new proof session, using directory given as argument
(** starts a new proof session, using directory given as argument
this reloads the previous session database if any.
Opening a session must be done prior to any other actions.
......@@ -183,64 +185,55 @@ module Make(O: OBSERVER) : sig
val maximum_running_proofs : int ref
val save_session : unit -> unit
(** enforces to save the session state on disk.
this it supposed to be called only at exit,
since the session manager also performs automatic saving
(** enforces to save the session state on disk.
this it supposed to be called only at exit,
since the session manager also performs automatic saving
some time to time *)
val file_exists : string -> bool
val add_file : string -> unit
(** [add_file adds the file [f] in the proof session,
(** [add_file f] adds the file [f] in the proof session,
the file name must be given relatively to the session dir
given to [open_session] *)
val get_all_files : unit -> file list
(* TODO
val reload_files : unit -> unit
(** reloads all the files in the state, and performs the proper
merging of old proof attemps and transformations *)
*)
(** {2 Actions} *)
(*****************************)
(* *)
(* actions *)
(* *)
(*****************************)
val apply_transformation : callback:(Task.task list -> unit) ->
transformation_data -> Task.task -> unit
val run_prover : context_unproved_goals_only:bool ->
val run_prover : context_unproved_goals_only:bool ->
prover_data -> any -> unit
(** [run_prover p a] runs prover [p] on all goals under [a] *)
val transform : context_unproved_goals_only:bool ->
val transform : context_unproved_goals_only:bool ->
transformation_data -> any -> unit
(** [apply_transformation tr a] applies transformation [trp]
(** [apply_transformation tr a] applies transformation [trp]
on all goals under [a] *)
val edit_proof :
val edit_proof :
default_editor:string -> project_dir:string -> proof_attempt -> unit
(** edit the given proof attempt using the appropriate editor *)
val replay :
obsolete_only:bool ->
val replay :
obsolete_only:bool ->
context_unproved_goals_only:bool -> any -> unit
(** [replay a] reruns proofs under [a]
(** [replay a] reruns proofs under [a]
if obsolete_only is set then does not rerun non-obsolete proofs
if context_unproved_goals_only is set then reruns only proofs with result was 'valid'
if context_unproved_goals_only is set then reruns only proofs
with result was 'valid'
*)
val reload_all: prover_data Util.Mstr.t -> unit
(** reloads all the files
(** reloads all the files
If for one of the file, the parsing or typing fails, then
the complete old session state is kept, and an exception
is raised
*)
(*
TODO
val remove_proof_attempt : proof_attempt -> unit
......@@ -250,7 +243,6 @@ TODO
(** [clean a] removes failed attempts below [a] where
there at least one successful attempt or transformation *)
*)
end
......
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