Commit 8dddf3f8 authored by MARCHE Claude's avatar MARCHE Claude

in progress: detached nodes

the concept of 'copy detached' disappears

theory nodes in sessions do not have any specific field 'detached goals' anymore
parent d2398547
......@@ -1425,18 +1425,10 @@ let paste () =
| None -> ())
| _ -> ()
let detached_copy () =
match get_selected_row_references () with
| [r] -> let n = get_node_id r#iter in
send_request (Copy_detached n)
| _ -> ()
let (_ : GMenu.menu_item) = exp_factory#add_item ~callback:copy "Copy"
let (_ : GMenu.menu_item) = exp_factory#add_item ~callback:paste "Paste"
let (_ : GMenu.menu_item) = exp_factory#add_item ~callback:detached_copy "Detached copy"
(*********************************)
(* add a new file in the project *)
(*********************************)
......
......@@ -182,7 +182,7 @@ module PSession = struct
List.fold_right
(fun g -> n (Goal g))
(theory_goals th)
(List.fold_right (fun g -> n (Goal g)) (theory_detached_goals th) [])
[]
| Goal id ->
let gid = get_proof_name s id in
let name = gid.Ident.id_string in
......@@ -859,24 +859,6 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
| _ -> raise BadCopyPaste
let copy_detached ~copy c from_any =
match from_any with
| APn from_pn ->
begin
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 "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
(* Only goal can be detached *)
| _ -> raise (BadCopyDetached "copy_detached. Can only copy goal")
......
......@@ -277,9 +277,6 @@ val copy_paste:
callback_tr:(string -> string list -> transformation_status -> unit) ->
controller -> any -> any -> unit
val copy_detached:
copy:(parent:any -> any -> unit) ->
controller -> any -> unit
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
......
......@@ -111,7 +111,6 @@ type ide_request =
| Unfocus_req
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
| Save_file_req of string * string
| Get_first_unproven_node of node_ID
| Save_req
......@@ -123,7 +122,6 @@ type ide_request =
let modify_session (r: ide_request) =
match r with
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Copy_detached _ -> true
| Set_config_param _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Save_req | Reload_req | Exit_req
......
......@@ -127,7 +127,6 @@ type ide_request =
| Unfocus_req
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
| Save_file_req of string * string
(** [Save_file_req(filename, content_of_file)] saves the file *)
| Get_first_unproven_node of node_ID
......
......@@ -268,7 +268,6 @@ let print_request fmt r =
| Unfocus_req -> fprintf fmt "unfocus"
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
| Copy_detached _ -> fprintf fmt "copy detached"
| Save_file_req _ -> fprintf fmt "save file"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
......@@ -1317,14 +1316,6 @@ end
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any
| Copy_detached from_id ->
let from_any = any_from_node_ID from_id in
let copy ~parent p =
let parent = node_ID_from_any parent in
ignore (new_node ~parent p)
in
C.copy_detached ~copy d.cont from_any
| Get_file_contents f ->
read_and_send f
| Save_file_req (name, text) ->
......
......@@ -152,7 +152,6 @@ let convert_request_constructor (r: ide_request) =
| Get_task _ -> String "Get_task"
| Remove_subtree _ -> String "Remove_subtree"
| Copy_paste _ -> String "Copy_paste"
| Copy_detached _ -> String "Copy_detached"
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Save_req -> String "Save_req"
| Reload_req -> String "Reload_req"
......@@ -189,9 +188,6 @@ let print_request_to_json (r: ide_request): Json_base.json =
convert_record ["ide_request", cc r;
"node_ID1", Int from_id;
"node_ID2", Int to_id]
| Copy_detached from_id ->
convert_record ["ide_request", cc r;
"node_ID", Int from_id]
| Get_first_unproven_node id ->
convert_record ["ide_request", cc r;
"node_ID", Int id]
......@@ -456,9 +452,6 @@ let parse_request (constr: string) j =
let to_id = get_int (get_field j "node_ID2") in
Copy_paste (from_id, to_id)
| "Copy_detached" ->
let n = get_int (get_field j "node_ID") in
Copy_detached n
| "Save_req" ->
Save_req
| "Reload_req" ->
......
......@@ -37,16 +37,14 @@ let print_proofAttemptID fmt id =
type theory = {
theory_name : Ident.ident;
theory_goals : proofNodeID list;
mutable theory_goals : proofNodeID list;
theory_parent_name : string;
theory_is_detached : bool;
mutable theory_detached_goals : proofNodeID list;
mutable theory_checksum : Termcode.checksum option;
}
let theory_name t = t.theory_name
let theory_goals t = t.theory_goals
let theory_detached_goals t = t.theory_detached_goals
type proof_parent = Trans of transID | Theory of theory
......@@ -576,7 +574,6 @@ let mk_proof_node ~version ~expl (s : session) (n : Ident.ident) (t : Task.task)
let shape = Termcode.t_shape_task ~version ~expl t in
let pn = { proofn_name = n;
proofn_expl = expl;
(* proofn_table = Some tables; *)
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
......@@ -589,7 +586,6 @@ let mk_proof_node_no_task (s : session) (n : Ident.ident)
(parent : proof_parent) (node_id : proofNodeID) sum shape proved =
let pn = { proofn_name = n;
proofn_expl = "";
(* proofn_table = None; *)
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
......@@ -598,32 +594,6 @@ let mk_proof_node_no_task (s : session) (n : Ident.ident)
Hint.add s.proofNode_table node_id pn;
Hint.add s.pn_state node_id proved
(* Detach a new proof to a proof_parent *)
let graft_detached_proof_on_parent s (pn: proofNodeID) (parent: proof_parent) =
match parent with
| Theory th ->
th.theory_detached_goals <- th.theory_detached_goals @ [pn]
| Trans tr_id ->
let tr = get_transfNode s tr_id in
tr.transf_detached_subtasks <- tr.transf_detached_subtasks @ [pn]
(* Intended as a feature to save a proof (also for testing detached stuff) *)
let copy_proof_node_as_detached (s: session) (pn_id: proofNodeID) =
let pn = get_proofNode s pn_id in
let new_pn_id = gen_proofNodeID s in
let parent = pn.proofn_parent in
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 _: unit = mk_proof_node_no_task s new_goal parent new_pn_id checksum shape false in
graft_detached_proof_on_parent s new_pn_id parent;
new_pn_id
let _mk_proof_node_task (s : session) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
let name,_,_ = Termcode.goal_expl_task ~root:false t in
mk_proof_node ~version:s.session_shape_version s name t parent node_id
let mk_transf_proof_node (s : session) (parent_name : string)
(tid : transID) (index : int) (t : Task.task) =
let id = gen_proofNodeID s in
......@@ -646,8 +616,6 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
Htn.add s.tn_state node_id proved;
pn.proofn_transformations <- node_id::pn.proofn_transformations
exception BadCopyDetached of string
let rec copy_structure ~notification s from_any to_any : unit =
match from_any, to_any with
| APn from_id, APn to_id ->
......@@ -682,7 +650,8 @@ 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 "copy_structure")
| _ -> failwith "Session_itp.copy_structure"
let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : string list) (tl : Task.task list) =
......@@ -1117,7 +1086,7 @@ let load_theory session parent_name old_provers acc th =
theory_is_detached = true;
theory_goals = goals;
theory_parent_name = parent_name;
theory_detached_goals = [] } in
} in
List.iter2
(load_goal session old_provers (Theory mth))
th.Xml.elements goals;
......@@ -1394,8 +1363,7 @@ let save_detached_theory parent_name old_s detached_theory s =
theory_checksum = None;
theory_is_detached = true;
theory_goals = goalsID;
theory_parent_name = parent_name;
theory_detached_goals = [] }
theory_parent_name = parent_name }
let merge_proof new_s ~goal_obsolete new_goal _ old_pa_n =
let old_pa = old_pa_n in
......@@ -1582,7 +1550,7 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
associated;
(* store the detached goals *)
let detached = List.map (fun (a,_) -> a) detached in
th.theory_detached_goals <- save_detached_goals old_s detached s (Theory th);
th.theory_goals <- th.theory_goals @ save_detached_goals old_s detached s (Theory th);
(* If we are not using shapes, we want to recover the goals that were
"wrongly" marked as obsolete during AssoGoals.simple_associate. The
condition for this to be correct is to check that the checksum of the
......@@ -1623,7 +1591,7 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
theory_is_detached = detached;
theory_goals = goalsID;
theory_parent_name = parent_name;
theory_detached_goals = [] } in
} in
let parent = Theory theory in
List.iter2 (add_goal parent) tasks goalsID;
begin
......
......@@ -65,7 +65,6 @@ val file_theories : file -> theory list
(** Theory *)
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file
type proof_attempt_node = private {
......@@ -233,10 +232,7 @@ val load_session : string -> session * bool
(** {2 Copy and remove} *)
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
val copy_structure: notification:(parent:any -> any -> unit) -> session -> any -> any -> unit
......
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