Commit c7afa200 authored by MARCHE Claude's avatar MARCHE Claude

ITP: better semantics of clean

parent e2f51d1a
This diff is collapsed.
......@@ -118,18 +118,20 @@ let send_request r =
let backtrace_and_exit f () =
try f () with
| e ->
if Debug.test_flag debug_stack_trace then
begin
Printexc.print_backtrace stdout;
exit 1
end
else
begin
Format.eprintf "Following exception %a was catched by Labelgtk."
Exn_printer.exn_printer e;
Format.eprintf "This should not happen. Please report. @.";
raise e
end
if Debug.test_flag debug_stack_trace then
begin
Printexc.print_backtrace stderr;
Format.eprintf "exception '%a' was raised in a LablGtk callback.@."
Exn_printer.exn_printer e;
exit 1
end
else
begin
Format.eprintf "exception '%a' was raised in a LablGtk callback.@."
Exn_printer.exn_printer e;
Format.eprintf "This should not happen. Please report. @.";
raise e
end
module S = struct
......
......@@ -661,31 +661,20 @@ let schedule_tr_with_same_arguments
let name = get_transf_name s tr in
schedule_transformation c pn name args ~callback ~notification
let is_valid (pa: proof_attempt_node) : bool =
match pa.Session_itp.proof_state with
| None -> false
| Some pr ->
begin
match pr.Call_provers.pr_answer with
| Call_provers.Valid -> true
| _ -> false
end
let is_running (pa: proof_attempt_node) : bool =
match pa.Session_itp.proof_state with
| None -> true
| Some _pr -> false
let clean_session c ~remove ~notification =
let clean_session c ~remove =
let s = c.controller_session in
Session_itp.session_iter_proof_attempt
(fun _ pa ->
let pnid = pa.parent in
Hprover.iter (fun _ paid ->
let npa = get_proof_attempt_node s paid in
if (not (is_valid npa) && not (is_running npa)) then
remove_subtree c ~removed:remove ~notification (APa paid))
(get_proof_attempt_ids s pnid))
(fun id pa ->
if pn_proved c pa.parent then
match pa.Session_itp.proof_state with
| None -> ()
| Some pr ->
if pa.Session_itp.proof_obsolete ||
Call_provers.(pr.pr_answer <> Valid)
then
remove_subtree c ~removed:remove ~notification:(fun _ -> ()) (APa id))
s
(* This function folds on any subelements of given node and tries to mark all
......
......@@ -219,9 +219,9 @@ val run_strategy_on_goal :
val clean_session:
controller ->
remove:(any -> unit) ->
notification:notifier -> unit
(** Remove proof_attempts that are not valid from the session *)
remove:(any -> unit) -> unit
(** Remove proof_attempts below proved goals, although thet are either obsoloete or not valid
*)
val mark_as_obsolete:
notification:notifier ->
......
......@@ -988,16 +988,11 @@ let get_locations t =
(* ----------------- Clean session -------------------- *)
let clean_session () =
let d = get_server_data () in
(*
let notification x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Proved b)) in
*)
let remove x =
let nid = node_ID_from_any x in
remove_any_node_ID x;
P.notify (Remove nid) in
C.clean_session d.cont ~remove ~notification:(notify_change_proved d.cont)
C.clean_session d.cont ~remove
(* ----------------- Save session --------------------- *)
......
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