Commit a31b9643 authored by Sylvain Dailler's avatar Sylvain Dailler

Minor. Debugging of copy_paste.

parent a4d4e60a
......@@ -763,13 +763,14 @@ let copy_detached ~copy c from_any =
let pn_id = copy_proof_node_as_detached c.controller_session from_pn in
let parent = get_any_parent c.controller_session from_any in
match parent with
| None -> raise BadCopyDetached
| None -> raise (BadCopyDetached "copy_detached no parent")
| Some parent ->
copy ~parent (APn pn_id);
copy_structure
~notification:copy c.controller_session (APn from_pn) (APn pn_id)
end
| _ -> raise BadCopyDetached (* Only goal can be detached *)
(* Only goal can be detached *)
| _ -> raise (BadCopyDetached "copy_detached. Can only copy goal")
let replay_proof_attempt c pr limit (id: proofNodeID) ~callback =
......
......@@ -568,7 +568,7 @@ let copy_proof_node_as_detached (s: session) (pn_id: proofNodeID) =
let new_goal = Ident.id_register (Ident.id_clone pn.proofn_name) in
let checksum = pn.proofn_checksum in
let shape = pn.proofn_shape in
let _ = mk_proof_node_no_task s new_goal parent new_pn_id checksum shape in
let (_: unit) = mk_proof_node_no_task s new_goal parent new_pn_id checksum shape in
graft_detached_proof_on_parent s new_pn_id parent;
new_pn_id
......@@ -602,7 +602,7 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
Hint.add s.trans_table node_id tn;
pn.proofn_transformations <- node_id::pn.proofn_transformations
exception BadCopyDetached
exception BadCopyDetached of string
let rec copy_structure ~notification s from_any to_any : unit =
match from_any, to_any with
......@@ -637,7 +637,7 @@ let rec copy_structure ~notification s from_any to_any : unit =
pn_id) sub_tasks in
let tr = get_transfNode s to_tn in
tr.transf_detached_subtasks <- new_sub_tasks
| _ -> raise BadCopyDetached
| _ -> raise (BadCopyDetached "copy_structure")
let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : string list) (tl : Task.task list) =
......
......@@ -98,7 +98,7 @@ val get_any_parent: session -> any -> any option
(* Answers true if a node is in a detached subtree *)
val is_detached: session -> any -> bool
exception BadCopyDetached
exception BadCopyDetached of string
(** [copy s pn] copy pn and add the copy as detached subgoal of its parent *)
val copy_proof_node_as_detached: session -> proofNodeID -> proofNodeID
......
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