Commit c989ee59 authored by François Bobot's avatar François Bobot

ide: add copy/paste facilities

parent 078cf0ac
......@@ -1051,6 +1051,49 @@ let apply_bisect_on_selection () =
S.iter_proof_attempt bisect_proof_attempt a
) (get_selected_row_references ())
(**************************************)
(* Copy Paste proof, transf and metas *)
(**************************************)
let copy_queue = Queue.create ()
let copy_on_selection () =
Queue.clear copy_queue;
List.iter
(fun r ->
let a = get_any_from_row_reference r in
let rec add = function
| S.Goal g -> S.goal_iter add g
| S.Transf f -> Queue.push (S.Transf (S.copy_transf f)) copy_queue
| S.Metas m -> Queue.push (S.Metas (S.copy_metas m)) copy_queue
| S.Proof_attempt pa ->
Queue.push (S.Proof_attempt (S.copy_proof pa)) copy_queue
| _ -> () in
add a
) (get_selected_row_references ())
let paste_on_selection () =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
match a with
| S.Goal g ->
let keygen = MA.keygen in
let rec paste = function
| S.Transf f ->
MA.init_any
(S.Transf (S.add_transf_to_goal ~keygen (env_session()) g f))
| S.Metas m ->
MA.init_any
(S.Metas (S.add_metas_to_goal ~keygen (env_session()) g m))
| S.Proof_attempt pa ->
MA.init_any (S.Proof_attempt
(S.add_proof_to_goal ~keygen (env_session()) g pa))
| _ -> () in
Queue.iter paste copy_queue
| _ -> ()
) (get_selected_row_references ())
(*********************************)
(* add a new file in the project *)
......@@ -1446,7 +1489,18 @@ let () =
~label:"Bisect in selection"
~callback:apply_bisect_on_selection
() : GMenu.image_menu_item) in
let add_copy_past_item () =
ignore(tools_factory#add_image_item
~label:"Copy"
~callback:copy_on_selection
() : GMenu.image_menu_item);
ignore(tools_factory#add_image_item
~label:"Paste"
~callback:paste_on_selection
() : GMenu.image_menu_item) in
add_refresh_provers add_separator "add separator in tools menu";
add_refresh_provers add_copy_past_item "add copy paste item";
add_refresh_provers add_separator "add separator in tools menu";
add_refresh_provers add_item_split "add split in tools menu";
add_refresh_provers add_item_inline "add inline in tools menu";
......@@ -1458,6 +1512,8 @@ let () =
add_refresh_provers add_item_bisect "add bisect in tools menu";
(** execute them *)
add_separator ();
add_copy_past_item ();
add_separator ();
add_item_split ();
add_item_inline ();
add_submenu_transform true ();
......
......@@ -2081,7 +2081,6 @@ let merge_file ~keygen ~theories env ~allow_obsolete from_f to_f =
to_f.file_theories;
dprintf debug "[Info] merge_file, done@\n"
let rec recompute_all_shapes_goal g =
let t = goal_task g in
g.goal_shape <- Termcode.t_shape_buf (Task.task_goal_fmla t);
......@@ -2141,6 +2140,127 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
= Termcode.current_shape_version);
new_env_session, obsolete
(** Copy/Paste *)
let rec copy_goal parent from_g =
let to_g = { from_g with
goal_parent = parent;
goal_external_proofs =
PHprover.create (PHprover.length from_g.goal_external_proofs);
goal_transformations =
PHstr.create (PHstr.length from_g.goal_transformations);
goal_metas = Mmetas_args.empty;
} in
PHprover.iter (fun k p -> PHprover.add to_g.goal_external_proofs
k (copy_proof to_g p)) from_g.goal_external_proofs;
PHstr.iter (fun k t -> PHstr.add to_g.goal_transformations
k (copy_transf to_g t)) from_g.goal_transformations;
to_g.goal_metas <- Mmetas_args.map
(fun m -> copy_metas to_g m) from_g.goal_metas;
to_g
and copy_proof to_goal from_pa =
{ from_pa with proof_parent = to_goal}
and copy_transf to_goal from_transf =
let to_transf = { from_transf with
transf_parent = to_goal;
transf_goals = []
} in
to_transf.transf_goals <-
List.map (copy_goal (Parent_transf from_transf))
from_transf.transf_goals;
to_transf
and copy_metas to_goal from_metas =
let to_metas = { from_metas with
metas_goal = to_goal;
} in
to_metas.metas_goal <- copy_goal (Parent_metas to_metas)
from_metas.metas_goal;
to_metas
let copy_proof from_p = copy_proof from_p.proof_parent from_p
let copy_transf from_t = copy_transf from_t.transf_parent from_t
let copy_metas from_m = copy_metas from_m.metas_parent from_m
exception Paste_error
let rec add_goal_to_parent ~keygen env from_goal to_goal =
set_goal_expanded to_goal from_goal.goal_expanded;
PHprover.iter (fun _ pa -> ignore (add_proof_to_goal ~keygen env to_goal pa))
from_goal.goal_external_proofs;
PHstr.iter (fun _ t -> ignore (add_transf_to_goal ~keygen env to_goal t))
from_goal.goal_transformations;
Mmetas_args.iter (fun _ m -> ignore (add_metas_to_goal ~keygen env to_goal m))
from_goal.goal_metas
(** This function is the main difference with merge_metas_aux.
It use directly the metas doesn't convert them.
*)
and add_metas_to_goal ~keygen env to_goal from_metas =
let to_metas = raw_add_metas ~keygen to_goal
from_metas.metas_added from_metas.metas_idpos
from_metas.metas_expanded in
let goal,task0 = Task.task_separate_goal (goal_task to_goal) in
(** add before the goal *)
let task =
try
Mstr.fold_left
(fun task name s ->
let m = Theory.lookup_meta name in
Smeta_args.fold_left
(fun task l -> Task.add_meta task m l) (** TODO: try with *)
task s)
task0 from_metas.metas_added
with exn ->
dprintf debug "[Paste] addition of metas produces an error:%a"
Exn_printer.exn_printer exn;
raise Paste_error in
let task = add_tdecl task goal in
let to_goal =
raw_add_task ~version:env.session.session_shape_version
~keygen (Parent_metas to_metas)
from_metas.metas_goal.goal_name
from_metas.metas_goal.goal_expl task false in
to_metas.metas_goal <- to_goal;
add_goal_to_parent ~keygen env from_metas.metas_goal to_goal;
to_metas
and add_proof_to_goal ~keygen env to_goal from_proof_attempt =
copy_external_proof ~keygen ~obsolete:true ~env_session:env ~goal:to_goal
from_proof_attempt
and add_transf_to_goal ~keygen env to_goal from_transf =
let from_transf_name = from_transf.transf_name in
let to_goal_name = to_goal.goal_name in
dprintf debug "[Paste] transformation %s for goal %s @\n"
from_transf_name to_goal_name.Ident.id_string;
let to_transf =
try
add_registered_transformation
~keygen env from_transf_name to_goal
with exn when not (Debug.test_flag Debug.stack_trace) ->
dprintf debug "[Paste] transformation %s produce an error:%a"
from_transf_name Exn_printer.exn_printer exn;
raise Paste_error
in
let associated =
dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate from_transf.transf_goals to_transf.transf_goals in
List.iter (function
| (to_goal, Some from_goal, _obsolete) ->
add_goal_to_parent ~keygen env from_goal to_goal
| (_, None, _) -> ()
) associated;
to_transf
(**)
let get_project_dir fname =
if not (Sys.file_exists fname) then raise Not_found;
let d =
......
......@@ -184,6 +184,8 @@ val get_project_dir : string -> string
return {Not_found} if the file or the directory doesn't exists
*)
(** {2 Read/Write} *)
type notask
(** A phantom type which is used for session which doesn't contain task. The
only session that can not contain task are session that come from the
......@@ -250,6 +252,24 @@ val update_session : keygen:'a keygen ->
*)
(** {2 Copy/Paste } *)
val copy_proof: 'a proof_attempt -> 'a proof_attempt
val copy_transf: 'a transf -> 'a transf
val copy_metas: 'a metas -> 'a metas
(** keys are copied *)
val add_proof_to_goal :
keygen:'a keygen -> 'a env_session ->
'a goal -> 'a proof_attempt ->'a proof_attempt
val add_transf_to_goal:
keygen:'a keygen -> 'a env_session ->
'a goal -> 'a transf -> 'a transf
val add_metas_to_goal :
keygen:'a keygen -> 'a env_session ->
'a goal -> 'a metas -> 'a metas
(** keys are normally generated *)
(** {2 Accessor} *)
exception NoTask
......@@ -366,7 +386,7 @@ val copy_external_proof :
{ul
{- the goal is not modified}
{- the prover is not modified}
{- a session or env_session is given}
{- a session is given}
}
The edited file is regenerated if
{ul
......
......@@ -769,6 +769,7 @@ module Hashtbl = struct
exception Key_not_found of key
val find' : 'a t -> key -> 'a
val set : unit t -> key -> unit
val map : ('a -> 'b) -> 'a t -> 'b t
end
module Make (X:Hashtbl.HashedType) = struct
......@@ -791,5 +792,10 @@ module Hashtbl = struct
let set h k = replace h k ()
let map f h =
let h' = create (length h) in
iter (fun k x -> add h' k (f x)) h;
h'
end
end
......@@ -485,6 +485,9 @@ module Hashtbl : sig
val set : unit t -> key -> unit
(** Add a binding that can be tested by mem *)
val map : ('a -> 'b) -> 'a t -> 'b t
(** just a shortcut not as efficient as doable *)
end
module Make (X:Hashtbl.HashedType) : S with type key = X.t
end
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