Commit 7bc5d591 authored by Sylvain Dailler's avatar Sylvain Dailler

When on transformation node, transformation apply to immediate children.

parent 78f71aa0
......@@ -1113,7 +1113,13 @@ end
let parent_id = get_proof_attempt_parent d.cont.controller_session panid in
let parent = node_ID_from_pn parent_id in
apply_transform parent t args
| ATn _ | AFile _ | ATh _ ->
| ATn tnid ->
let child_ids = get_sub_tasks d.cont.controller_session tnid in
let callback = callback_update_tree_transform t args in
List.iter (fun id -> C.schedule_transformation d.cont id t args ~callback
~notification:(notify_change_proved d.cont))
child_ids
| AFile _ | ATh _ ->
(* TODO: propagate trans to all subgoals, just the first one, do nothing ... ? *)
()
......
......@@ -400,7 +400,8 @@ let interp commands_table cont id s =
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
match id with
| Some (Session_itp.APn _id) -> Transform (cmd,t,args)
| _ -> QError ("Please select a goal node in the task tree")
| Some (Session_itp.ATn _tid) -> Transform (cmd, t, args)
| _ -> QError ("Please select a goal or trans node in the task tree")
with
| Trans.UnknownTrans _ ->
match parse_prover_name cont.Controller_itp.controller_config cmd args with
......
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