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

Merge branch 'new_ide' into master

This intends to add improvements that were done in new_ide but not merged
in master yet.
In particular, this merges
- the commit for interruption of provers in why3server.
- several counterexamples improvements:
  * choice of pretty printing for float counterexamples
  * countereamples parsing of lowercase "lambda"
- itp_server/controller_itp improvements:
  * error handling in itp_server (any_from_node_ID is now option)
  * reformating of controller_itp queues as record instead of tuples
  * choice to always give a new goal with the automatic function that gets
next goal

Conflicts:
	bench/ce/algebraic_type_CVC4,1.5.oracle
	bench/ce/algebraic_type_Z3,4.6.0.oracle
	bench/ce/array_records_CVC4,1.5.oracle
	bench/ce/array_records_Z3,4.6.0.oracle
	bench/ce/arrays_CVC4,1.5.oracle
	bench/ce/arrays_Z3,4.6.0.oracle
	bench/ce/floats_CVC4,1.5.oracle
	bench/ce/floats_Z3,4.6.0.oracle
	bench/ce/if_decision_branch.mlw
	bench/ce/if_decision_branch_CVC4,1.5.oracle
	bench/ce/if_decision_branch_Z3,4.6.0.oracle
	bench/ce/int.mlw
	bench/ce/int32_CVC4,1.5.oracle
	bench/ce/int32_Z3,4.6.0.oracle
	bench/ce/int_CVC4,1.5.oracle
	bench/ce/int_Z3,4.6.0.oracle
	bench/ce/int_overflow_CVC4,1.5.oracle
	bench/ce/int_overflow_Z3,4.6.0.oracle
	bench/ce/jlamp0_CVC4,1.5.oracle
	bench/ce/jlamp0_Z3,4.6.0.oracle
	bench/ce/jlamp_array_CVC4,1.5.oracle
	bench/ce/jlamp_array_Z3,4.6.0.oracle
	bench/ce/jlamp_projections_CVC4,1.5.oracle
	bench/ce/jlamp_projections_Z3,4.6.0.oracle
	bench/ce/map_CVC4,1.5.oracle
	bench/ce/map_Z3,4.6.0.oracle
	bench/ce/real_CVC4,1.5.oracle
	bench/ce/real_Z3,4.6.0.oracle
	bench/ce/record_map_CVC4,1.5.oracle
	bench/ce/record_map_Z3,4.6.0.oracle
	bench/ce/records_CVC4,1.5.oracle
	bench/ce/records_Z3,4.6.0.oracle
	bench/ce/ref_CVC4,1.5.oracle
	bench/ce/ref_Z3,4.6.0.oracle
	bench/ce/simple_array_CVC4,1.5.oracle
	bench/ce/simple_array_Z3,4.6.0.oracle
	src/core/ident.ml
	src/core/ident.mli
	src/parser/parser.mly
	src/printer/alt_ergo.ml
	src/printer/smtv2.ml
	src/session/itp_server.ml
	src/transform/eval_match.ml
	src/transform/intro_projections_counterexmp.ml
	src/transform/intro_vc_vars_counterexmp.ml
	src/whyml/mlw_wp.ml
	tests/demo-itp.mlw
parents fc1d0588 6bb006b9
......@@ -607,7 +607,7 @@ clean::
##############
SERVER_MODULES := logging arraylist options queue readbuf request \
writebuf server-unix server-win
proc writebuf server-unix server-win
CPULIM_MODULES := cpulimit-unix cpulimit-win
......
......@@ -368,7 +368,8 @@ let append_to_model_element_name ~attrs ~to_append =
let splitted = Strings.bounded_split '@' attr_str 2 in
match splitted with
| [before; after] -> before ^ to_append ^ "@" ^ after
| _ -> attr_str^to_append in
| _ -> attr_str^to_append
in
transform_model_trace_attr attrs trans
let append_to_model_trace_attr ~attrs ~to_append =
......
......@@ -37,8 +37,11 @@ type float_type =
| Float_hexa of string * float
let interp_float b eb sb =
let interp_float ?(interp=true) b eb sb =
try
(* We don't interpret when this is disable *)
if not interp then
raise Exit;
let is_neg = match b with
| "#b0" -> false
| "#b1" -> true
......
......@@ -24,7 +24,7 @@ type float_type =
| Float_value of string * string * string
| Float_hexa of string * float
val interp_float: string -> string -> string -> float_type
val interp_float: ?interp:bool -> string -> string -> string -> float_type
type model_value =
| Integer of string
......
......@@ -551,3 +551,5 @@ let call_editor ~command fin =
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in;
EditorCall pid
let interrupt_call id = Prove_client.send_interrupt ~id
......@@ -179,3 +179,5 @@ val query_call : prover_call -> prover_update
val wait_on_call : prover_call -> prover_result
(** blocking function that waits until the prover finishes. *)
val interrupt_call : int -> unit
......@@ -59,6 +59,7 @@ rule token = parse
| "true" { TRUE }
| "false" { FALSE }
| "LAMBDA" { LAMBDA }
| "lambda" { LAMBDA }
| "ARRAY_LAMBDA" { ARRAY_LAMBDA }
| "(_" space+ "bv"(num as bv_value) space+ num")" { BITVECTOR_VALUE bv_value }
| "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
......
......@@ -165,6 +165,14 @@ let send_request ~id ~timelimit ~memlimit ~use_stdin ~cmd =
let s = Buffer.contents send_buf in
send_request_string s
let send_interrupt ~id =
if not (is_connected ()) then connect_internal ();
Buffer.clear send_buf;
Buffer.add_string send_buf "interrupt;";
Buffer.add_string send_buf (string_of_int id);
let s = Buffer.contents send_buf in
send_request_string s
let rec read_lines blocking =
let s = read_from_client blocking in
(* TODO: should we detect and handle EOF here? *)
......
......@@ -42,6 +42,8 @@ val send_request :
cmd:string list ->
unit
val send_interrupt : id:int -> unit
type final_answer = {
id : int;
time : float;
......
#include <signal.h>
#include <stdlib.h>
#include <string.h>
#include "proc.h"
#include "options.h"
// global pointers are initialized with NULL by C semantics
plist processes;
// kill process using os specific routine
void os_kill(pproc p);
void os_kill(pproc p) {
#ifdef _WIN32
// arbitrarily chosen exit code
TerminateProcess(p->handle, ERROR_REQUEST_ABORTED);
#else
kill(p->id, SIGKILL);
#endif
}
void init_process_list () {
processes = init_list(parallel);
}
void kill_processes(char *id) {
for (int i = 0; i < processes->len; i++) {
if (!strcmp(((pproc)(processes->data[i]))->task_id, id)) {
os_kill((pproc)processes->data[i]);
}
}
}
void free_process(pproc proc) {
#ifdef _WIN32
CloseHandle(proc->handle);
CloseHandle(proc->job);
#endif
free(proc->outfile);
free(proc->task_id);
free(proc);
}
#ifndef PROC_H
#define PROC_H
#ifdef _WIN32
#include <windows.h>
#else
#include <sys/types.h>
#endif
#include "arraylist.h"
typedef struct {
#ifdef _WIN32
HANDLE handle;
HANDLE job;
#else
pid_t id;
#endif
int client_key;
char* task_id;
char* outfile;
} t_proc, *pproc;
extern plist processes;
// free memory and resources associated with the process p
void free_process(pproc p);
// kill all processes whose task_id is equal to id
void kill_processes(char *id);
// initialize global list of processes
void init_process_list();
#endif
......@@ -27,7 +27,6 @@
#include <poll.h>
#include <stddef.h>
#include <stdlib.h>
#include <string.h>
#include <signal.h>
#include <sys/time.h>
#include <sys/wait.h>
......@@ -41,6 +40,7 @@
#include "writebuf.h"
#include "options.h"
#include "logging.h"
#include "proc.h"
#define READ_ONCE 1024
......@@ -53,13 +53,6 @@ typedef struct {
int server_sock = -1;
typedef struct {
pid_t id;
int client_fd;
char* task_id;
char* outfile;
} t_proc, *pproc;
// the poll list is the list of file descriptors for which we monitor certain
// events.
struct pollfd* poll_list;
......@@ -67,7 +60,6 @@ int poll_num = 0;
int poll_len = 0;
// global pointers are initialized with NULL by C semantics
plist processes;
plist clients;
char *current_dir;
......@@ -275,7 +267,7 @@ void server_init_listening(char* socketname, int parallel) {
free(socketname_copy1);
free(socketname_copy2);
add_to_poll_list(server_sock, POLLIN);
processes = init_list(parallel);
init_process_list();
setup_child_pipe();
}
......@@ -427,12 +419,6 @@ void send_msg_to_client(pclient client,
queue_write(client, msgbuf);
}
void free_process(pproc proc) {
free(proc->outfile);
free(proc->task_id);
free(proc);
}
void handle_child_events() {
pproc child;
pclient client;
......@@ -461,7 +447,7 @@ void handle_child_events() {
}
child = (pproc) list_lookup(processes, pid);
list_remove(processes, pid);
client = (pclient) list_lookup(clients, child->client_fd);
client = (pclient) list_lookup(clients, child->client_key);
if (client != NULL) {
send_msg_to_client(client,
child->task_id,
......@@ -500,7 +486,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->task_id = r->id;
proc->client_fd = r->key;
proc->client_key = r->key;
proc->id = id;
proc->outfile = outfile;
list_append(processes, id, (void*) proc);
......@@ -538,8 +524,7 @@ void handle_msg(pclient client, int key) {
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
remove_from_queue(r->id);
// kill all processes whose id is r->id;
// TODO kill_processes(processes, r->id);
kill_processes(r->id);
free_request(r);
break;
}
......
......@@ -32,6 +32,7 @@
#include "writebuf.h"
#include "arraylist.h"
#include "logging.h"
#include "proc.h"
#define READ_ONCE 1024
#define BUFSIZE 4096
......@@ -62,14 +63,6 @@ typedef struct {
pwritebuf writebuf;
} t_client, *pclient;
typedef struct {
HANDLE handle;
HANDLE job;
int client_key;
char* id;
char* outfile;
} t_proc, *pproc;
// AFAIU, there is no connection queue or something like that, so we need to
// create several socket instances to be able to process several clients that
// would connect almost at the same time. The two variables below will be
......@@ -79,7 +72,6 @@ pserver* server_socket;
int* server_key;
plist clients;
plist processes;
char current_dir[MAX_PATH];
int gen_key = 1;
......@@ -109,7 +101,6 @@ HANDLE completion_port;
void shutdown_with_msg(char* msg);
void shutdown_with_msg(char* msg) {
pproc proc;
if (completion_port != NULL) {
CloseHandle (completion_port);
}
......@@ -125,9 +116,7 @@ void shutdown_with_msg(char* msg) {
}
if (processes != NULL) {
for (int i = 0; i < list_length(processes); i++) {
proc = processes->data[i];
CloseHandle(proc->handle);
CloseHandle(proc->job);
free_process(processes->data[i]);
}
}
logging_shutdown(msg);
......@@ -430,7 +419,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->handle = pi.hProcess;
proc->job = ghJob;
proc->id = r->id;
proc->task_id = r->id;
proc->client_key = r->key;
proc->outfile = outfile;
key = keygen();
......@@ -469,7 +458,10 @@ void handle_msg(pclient client, int key) {
break;
case REQ_INTERRUPT:
remove_from_queue(r->id);
// TODO: remove r from the queue if still there, or kill the process r->id;
kill_processes(r->id);
// no need to clean up the list of processes and free the memory for
// processes, this will be done when we get notified of the end of the
// child process
free_request(r);
break;
}
......@@ -502,14 +494,6 @@ void accept_client(int key, int socket_num) {
do_read(client);
}
void free_process(pproc proc) {
CloseHandle(proc->handle);
CloseHandle(proc->job);
free(proc->id);
free(proc->outfile);
free(proc);
}
void send_started_msg_to_client(pclient client,
char* id) {
char* msgbuf;
......@@ -621,7 +605,7 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
timeout = (exitcode == ERROR_NOT_ENOUGH_QUOTA) ||
(exitcode == STATUS_QUOTA_EXCEEDED);
send_msg_to_client(client,
child->id,
child->task_id,
exitcode,
cpu_time,
timeout,
......@@ -648,7 +632,7 @@ void init() {
init_request_queue();
clients = init_list(parallel);
processes = init_list(parallel);
init_process_list();
server_socket = (pserver*) malloc(parallel * sizeof(pserver));
server_key = (int*) malloc(parallel * sizeof(int));
......
......@@ -262,9 +262,34 @@ end
module Make(S : Scheduler) = struct
let scheduled_proof_attempts = Queue.create ()
(* type for scheduled proof attempts *)
type sched_pa_rec =
{ spa_contr : controller;
spa_id : proofNodeID;
spa_pr : Whyconf.prover;
spa_limit : Call_provers.resource_limit;
spa_pr_scr : string option;
spa_callback : (proof_attempt_status -> unit);
spa_ores : Call_provers.prover_result option;
}
let scheduled_proof_attempts : sched_pa_rec Queue.t = Queue.create ()
(* type for prover tasks in progress *)
type tasks_prog_rec =
{
tp_session : Session_itp.session;
tp_id : proofNodeID;
tp_pr : Whyconf.prover;
tp_callback : (proof_attempt_status -> unit);
tp_started : bool;
tp_call : Call_provers.prover_call;
tp_ores : Call_provers.prover_result option;
}
let prover_tasks_in_progress = Hashtbl.create 17
let prover_tasks_in_progress :
(Call_provers.prover_call,tasks_prog_rec) Hashtbl.t =
Hashtbl.create 17
(* We need to separate tasks that are edited from proofattempt in progress
because we are not using why3server for the edited proofs and timeout_handler
......@@ -282,9 +307,7 @@ let register_observer = (:=) observer
module Hprover = Whyconf.Hprover
(* calling provers, with limits adaptation
*)
(* calling provers, with limits adaptation *)
(* to avoid corner cases when prover results are obtained very closely
......@@ -356,28 +379,38 @@ let fuzzy_proof_time nres ores =
else nres
let build_prover_call ?proof_script c id pr limit callback ores =
let (config_pr,driver) = Hprover.find c.controller_provers pr in
let with_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let build_prover_call spa =
let c = spa.spa_contr in
let limit = spa.spa_limit in
let (config_pr,driver) = Hprover.find c.controller_provers spa.spa_pr in
let with_steps =
Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let command =
Whyconf.get_complete_command config_pr ~with_steps in
try
let task = Session_itp.get_task c.controller_session id in
let task = Session_itp.get_task c.controller_session spa.spa_id in
Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
(Pp.print_option Pp.string) proof_script;
(Pp.print_option Pp.string) spa.spa_pr_scr;
let inplace = config_pr.Whyconf.in_place in
let interactive = config_pr.Whyconf.interactive in
try
let call =
Driver.prove_task ?old:proof_script ~inplace ~command
~limit ~interactive driver task
Driver.prove_task ?old:spa.spa_pr_scr ~inplace ~command
~limit ~interactive driver task
in
let pa = (c.controller_session,id,pr,callback,false,call,ores) in
let pa =
{ tp_session = c.controller_session;
tp_id = spa.spa_id;
tp_pr = spa.spa_pr;
tp_callback = spa.spa_callback;
tp_started = false;
tp_call = call;
tp_ores = spa.spa_ores } in
Hashtbl.replace prover_tasks_in_progress call pa
with Sys_error _ as e ->
callback (InternalFailure e)
spa.spa_callback (InternalFailure e)
with Not_found (* goal has no task, it is detached *) ->
callback Detached
spa.spa_callback Detached
let update_observer () =
let scheduled = Queue.length scheduled_proof_attempts in
......@@ -393,31 +426,31 @@ let timeout_handler () =
let results = Call_provers.get_new_results ~blocking:S.blocking in
List.iter (fun (call, prover_update) ->
match Hashtbl.find prover_tasks_in_progress call with
| (ses,id,pr,callback,started,call,ores) ->
| ptp ->
begin match prover_update with
| Call_provers.NoUpdates -> ()
| Call_provers.ProverStarted ->
assert (not started);
callback Running;
assert (not ptp.tp_started);
ptp.tp_callback Running;
incr number_of_running_provers;
Hashtbl.replace prover_tasks_in_progress call
(ses,id,pr,callback,true,call,ores)
Hashtbl.replace prover_tasks_in_progress ptp.tp_call
{ptp with tp_started = true}
| Call_provers.ProverFinished res ->
Hashtbl.remove prover_tasks_in_progress call;
if started then decr number_of_running_provers;
let res = Opt.fold fuzzy_proof_time res ores in
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
let res = Opt.fold fuzzy_proof_time res ptp.tp_ores in
(* inform the callback *)
callback (Done res)
ptp.tp_callback (Done res)
| Call_provers.ProverInterrupted ->
Hashtbl.remove prover_tasks_in_progress call;
if started then decr number_of_running_provers;
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
(* inform the callback *)
callback (Interrupted)
ptp.tp_callback (Interrupted)
| Call_provers.InternalFailure exn ->
Hashtbl.remove prover_tasks_in_progress call;
if started then decr number_of_running_provers;
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
(* inform the callback *)
callback (InternalFailure (exn))
ptp.tp_callback (InternalFailure (exn))
end
| exception Not_found -> ()
(* We probably received ProverStarted after ProverFinished,
......@@ -454,12 +487,10 @@ let timeout_handler () =
try
for _i = Hashtbl.length prover_tasks_in_progress
to S.multiplier * !session_max_tasks do
let (c,id,pr,limit,proof_script,callback,ores) =
Queue.pop scheduled_proof_attempts in
try
build_prover_call ?proof_script c id pr limit callback ores
let spa = Queue.pop scheduled_proof_attempts in
try build_prover_call spa
with e when not (Debug.test_flag Debug.stack_trace) ->
callback (InternalFailure e)
spa.spa_callback (InternalFailure e)
done
with Queue.Empty -> ()
end;
......@@ -468,8 +499,7 @@ let timeout_handler () =
let interrupt () =
(* Interrupt provers *)
Hashtbl.iter (fun _k e ->
let (_, _, _, callback, _, _, _) = e in callback Interrupted)
Hashtbl.iter (fun _k e -> e.tp_callback Interrupted)
prover_tasks_in_progress;
Hashtbl.clear prover_tasks_in_progress;
(* Do not interrupt editors
......@@ -481,9 +511,8 @@ let interrupt () =
*)
number_of_running_provers := 0;
while not (Queue.is_empty scheduled_proof_attempts) do
let (_c,_id,_pr,_limit,_proof_script,callback,_ores) =
Queue.pop scheduled_proof_attempts in
callback Interrupted
let spa = Queue.pop scheduled_proof_attempts in
spa.spa_callback Interrupted
done;
!observer 0 0 0
......@@ -543,8 +572,15 @@ let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
with Not_found | Session_itp.BadID -> limit,None,save_to
in
let panid = graft_proof_attempt ~limit ses id pr in
Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,ores)
scheduled_proof_attempts;
let spa =
{ spa_contr = c;
spa_id = id;
spa_pr = pr;
spa_limit = adaptlimit;
spa_pr_scr = proof_script;
spa_callback = callback panid;
spa_ores = ores } in
Queue.add spa scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
......
......@@ -353,7 +353,9 @@ let () =
let model_any : any Hint.t = Hint.create 17
let any_from_node_ID (nid:node_ID) : any = Hint.find model_any nid
let any_from_node_ID (nid:node_ID) : any option =
try Some (Hint.find model_any nid) with
| Not_found -> None
let pan_to_node_ID : node_ID Hpan.t = Hpan.create 17
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
......@@ -519,7 +521,7 @@ module P = struct
(* true if nid is below f_node or does not exists (in which case the
notification is a remove). false if not below. *)
let is_below s nid f_nodes =
let any = try Some (any_from_node_ID nid) with _ -> None in
let any = any_from_node_ID nid in
match any with
| None -> true
| Some any ->
......@@ -852,6 +854,10 @@ end
let send_task nid show_full_context loc =
let d = get_server_data () in
let any = any_from_node_ID nid in
match any with
| None ->
P.notify (Message (Error "Please select a node id"))
| Some any ->
if Session_itp.is_detached d.cont.controller_session any then
match any with
| APn _id ->
......@@ -1079,28 +1085,37 @@ end
let d = get_server_data () in
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id prover
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
let any = any_from_node_ID nid in
match any with
| None -> P.notify (Message (Error "Please select a node id"))
| Some any ->
let unproven_goals = unproven_goals_below_id d.cont any in
List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id
prover ~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
let schedule_edition (nid: node_ID) (prover: Whyconf.prover) =
let d = get_server_data () in
let callback = callback_update_tree_proof d.cont in
try
let id =
match any_from_node_ID nid with
| APn id -> id
| APa panid -> get_proof_attempt_parent d.cont.controller_session panid
| _ -> raise Not_found
in
C.schedule_edition d.cont id prover
~callback ~notification:(notify_change_proved d.cont)
with Not_found ->
P.notify
(Message
(Error
"for edition you must select a proof attempt node"))
let any = any_from_node_ID nid in
match any with
| None -> P.notify (Message (Error "Please select a node id"));
| Some any ->
try
let id =
match any with
| APn id -> id
| APa panid ->
get_proof_attempt_parent d.cont.controller_session panid
| _ -> raise Not_found
in
C.schedule_edition d.cont id prover
~callback ~notification:(notify_change_proved d.cont)
with Not_found ->
P.notify
(Message
(Error
"for edition you must select a proof attempt node"))
(* ----------------- Schedule transformation -------------------- *)
......@@ -1152,7 +1167,10 @@ end
List.iter (fun id -> apply_transform (APn id) t args) child_ids
in
let nid = any_from_node_ID node_id in
apply_transform nid t args
match nid with
| None -> P.notify (Message (Error "Please select a node id"));
| Some nid ->
apply_transform nid t args
let removed x =
let nid = node_ID_from_any x in
......@@ -1165,7 +1183,7 @@ end
try
let id =
match any_from_node_ID nid with
| APa panid -> panid
| Some (APa panid) -> panid
| _ -> raise Not_found
in
let callback_pa = callback_update_tree_proof d.cont in
......@@ -1187,7 +1205,11 @@ end
let run_strategy_on_task nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
let any = any_from_node_ID nid in
match any with
| None -> P.notify (Message (Error "Please select a node id"));
| Some any ->
let unproven_goals = unproven_goals_below_id d.cont any in
try
let (n,_,_,st) = Hstr.find d.cont.controller_strategies s in
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
......@@ -1214,13 +1236,16 @@ end
let remove_node nid =
let d = get_server_data () in
let n = any_from_node_ID nid in
let any = any_from_node_ID nid in
match any with
| None -> P.notify (Message (Error "Please select a node id"))
| Some any ->
begin
try
remove_subtree
~notification:(notify_change_proved d.cont)
~removed
d.cont n
d.cont any
with RemoveError -> (* TODO send an error instead of information *)
P.notify (Message (Information "Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"))
end
......@@ -1293,8 +1318,12 @@ end
let notify_first_unproven_node d ni =
let s = d.cont.controller_session in
let any = any_from_node_ID ni in
match any with
| None -> P.notify (Message (Error "Please select a node id"))
| Some any ->
let unproven_any =
get_first_unproven_goal_around
~always_send:false
~proved:(Session_itp.any_proved s)
~children:(get_undetached_children_no_pa s)
~get_parent:(get_any_parent s)
......@@ -1351,15 +1380,21 @@ end
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
begin
try
C.copy_paste
~notification:(notify_change_proved d.cont)
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any;
session_needs_saving := true
with C.BadCopyPaste ->
P.notify (Message (Error "invalid copy"))
match from_any, to_any with
| None, _ | _, None ->
P.notify (Message (Error "Please select a node id"));
| Some from_any, Some to_any ->
begin
try
C.copy_paste
~notification:(notify_change_proved d.cont)
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any;
session_needs_saving := true
with C.BadCopyPaste ->
P.notify (Message (Error "invalid copy"))
end