Disallow copy paste of the same transformations under the same node

src/session/controller_itp.ml

@@ -659,6 +659,8 @@ let schedule_edition c id pr ~callback ~notification =
             prover_tasks_edited;
   run_timeout_handler ()
 
+exception TransAlreadyExists of string * string
+
 (*** { 2 transformations} *)
 
 let schedule_transformation c id name args ~callback ~notification =
@@ -690,6 +692,8 @@ let schedule_transformation c id name args ~callback ~notification =
     end;
     false
   in
+  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;
   callback TSscheduled
 
@@ -764,6 +768,7 @@ let schedule_tr_with_same_arguments
   let args = get_transf_args s tr in
   let name = get_transf_name s tr in
   let callback = callback name args in
+
   schedule_transformation c pn name args ~callback ~notification
 
 let proof_is_complete pa =

src/session/controller_itp.mli

@@ -231,6 +231,7 @@ val prepare_edition :
     of node [id] with prover [pr], using the file name given. The
     editor is not launched. *)
 
+exception TransAlreadyExists of string * string
 
 val schedule_transformation :
   controller ->

src/session/itp_server.ml

@@ -1130,16 +1130,10 @@ end
   let apply_transform node_id t args =
     let d = get_server_data () in
 
-    let check_if_already_exists s pid t args =
-      let sub_transfs = get_transformations s pid in
-      List.exists (fun tr_id -> get_transf_name s tr_id = t && get_transf_args s tr_id = args &&
-        not (is_detached s (ATn tr_id))) sub_transfs
-    in
-
     let rec apply_transform nid t args =
       match nid with
       | APn id ->
-        if check_if_already_exists d.cont.controller_session id t args then
+        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
@@ -1444,7 +1438,11 @@ end
        end
     | Exit_req                -> exit 0
      )
-    with e when not (Debug.test_flag Debug.stack_trace)->
+    with
+    | C.TransAlreadyExists (name,args) ->
+        P.notify (Message (Error
+          (Pp.sprintf "Transformation %s with arg [%s] already exists" name args)))
+    | e when not (Debug.test_flag Debug.stack_trace)->
       P.notify (Message (Error (Pp.string_of
           (fun fmt (r,e) -> Format.fprintf fmt
              "There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"

src/session/session_itp.ml

@@ -325,6 +325,11 @@ let set_obsolete s paid b =
   let pa = get_proof_attempt_node s paid in
   pa.proof_obsolete <- b
 
+let check_if_already_exists s pid t args =
+    let sub_transfs = get_transformations s pid in
+    List.exists (fun tr_id ->
+      get_transf_name s tr_id = t && get_transf_args s tr_id = args &&
+      not (is_detached s (ATn tr_id))) sub_transfs
 
 (* Iterations functions on the session tree *)
 

src/session/session_itp.mli

@@ -119,6 +119,9 @@ val is_detached: session -> any -> bool
 val get_encapsulating_theory: session -> any -> theory
 val get_encapsulating_file: session -> any -> file
 
+(* Check if a transformation already exists *)
+val check_if_already_exists:
+    session -> proofNodeID -> string -> string list -> bool
 
 (** {2 iterators on sessions} *)