Commit b4b7fb39 authored by Sylvain Dailler's avatar Sylvain Dailler

Avoid popup failing when applying transformation on a detached node

parent 75e59ea1
......@@ -717,6 +717,7 @@ let schedule_edition c id pr ~callback ~notification =
run_timeout_handler ()
exception TransAlreadyExists of string * string
exception GoalNodeDetached of proofNodeID
(*** { 2 transformations} *)
......@@ -757,6 +758,8 @@ let schedule_transformation c id name args ~callback ~notification =
end;
false
in
if Session_itp.is_detached c.controller_session (APn id) then
raise (GoalNodeDetached id);
if Session_itp.check_if_already_exists c.controller_session id name args then
raise (TransAlreadyExists (name, List.fold_left (fun acc s -> s ^ " " ^ acc) "" args));
S.idle ~prio:0 apply_trans;
......
......@@ -248,6 +248,7 @@ val prepare_edition :
session directory, and [res] is the former result if any. *)
exception TransAlreadyExists of string * string
exception GoalNodeDetached of proofNodeID
val schedule_transformation :
controller ->
......
......@@ -1154,12 +1154,15 @@ end
let rec apply_transform nid t args =
match nid with
| APn id ->
if Session_itp.check_if_already_exists d.cont.controller_session id t args then
P.notify (Message (Information "Transformation already applied"))
if Session_itp.is_detached d.cont.controller_session nid then
P.notify (Message (Information "Transformation cannot apply on detached node"))
else
let callback = callback_update_tree_transform t args in
C.schedule_transformation d.cont id t args ~callback
~notification:(notify_change_proved d.cont)
if Session_itp.check_if_already_exists d.cont.controller_session id t args then
P.notify (Message (Information "Transformation already applied"))
else
let callback = callback_update_tree_transform t args in
C.schedule_transformation d.cont id t args ~callback
~notification:(notify_change_proved d.cont)
| APa panid ->
let parent_id = get_proof_attempt_parent d.cont.controller_session panid in
apply_transform (APn parent_id) t args
......@@ -1513,6 +1516,11 @@ end
(Error
(Pp.sprintf "Transformation %s with arg [%s] already exists"
name args)))
| C.GoalNodeDetached _id ->
P.notify
(Message
(Information
("Transformation cannot apply on detached node")))
| e when not (Debug.test_flag Debug.stack_trace)->
P.notify
(Message
......
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