Commit 1456ecb9 authored by Sylvain Dailler's avatar Sylvain Dailler

Extend mark obsolete to all possible nodes.

parent 9e43e390
......@@ -702,18 +702,24 @@ let clean_session c ~remove ~node_change =
remove_subtree c ~removed:remove ~node_change (APa paid))
(get_proof_attempt_ids s pnid)) s
(* This function folds on any subelements of given node and tries to mark all
proof attempts it encounters *)
let mark_as_obsolete ~node_change ~node_obsolete c any =
let s = c.controller_session in
match any with
| APa n ->
(* Case for proof attempt only *)
let mark_as_obsolete_pa ~node_change ~node_obsolete c n =
let s = c.controller_session in
let parent = get_proof_attempt_parent s n in
Session_itp.mark_obsolete s n;
node_obsolete any true;
node_obsolete (APa n) true;
let b = reload_goal_proof_state c parent in
node_change (APn parent) b;
update_proof_node node_change c parent b
| _ -> ()
in
let s = c.controller_session in
fold_all_any s
(fun () any -> match any with
| APa n -> mark_as_obsolete_pa ~node_change ~node_obsolete c n
| _ -> ()) () any
exception BadCopyPaste
......
......@@ -182,3 +182,6 @@ val remove_subtree: session -> any -> notification:(any -> unit) -> unit
session s then call the notification function (used to notify the ide.
If called on a theory or proof node, raise RemoveError *)
val fold_all_any: session -> ('a -> any -> 'a) -> 'a -> any -> 'a
(** [fold_all_any s f acc any] folds on all the subnodes of any *)
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