Skip to content
Snippets Groups Projects
Commit e662156f authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

itp_server: any_from_node_ID now returns an option type 

This helps when an IDE wants to send a command with no node_id selected
(root_node is chosen and it does not happen to be in model_any).
parent c801b15c
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/session/itp_server.ml
+ 79
− 41
View file @ e662156f
......@@ -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 ->
......@@ -1068,19 +1074,28 @@ 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))
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
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_from_node_ID nid with
match any with
| APn id -> id
| APa panid -> get_proof_attempt_parent d.cont.controller_session panid
| APa panid ->
get_proof_attempt_parent d.cont.controller_session panid
| _ -> raise Not_found
in
C.schedule_edition d.cont id prover
......@@ -1141,6 +1156,9 @@ end
List.iter (fun id -> apply_transform (APn id) t args) child_ids
in
let nid = any_from_node_ID node_id in
match nid with
| None -> P.notify (Message (Error "Please select a node id"));
| Some nid ->
apply_transform nid t args
let removed x =
......@@ -1154,7 +1172,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
......@@ -1176,7 +1194,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;
......@@ -1203,13 +1225,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
......@@ -1282,6 +1307,9 @@ 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
~proved:(Session_itp.any_proved s)
......@@ -1352,6 +1380,11 @@ end
| Copy_paste (from_id, to_id) ->
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
begin
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
......@@ -1362,6 +1395,7 @@ end
with C.BadCopyPaste ->
P.notify (Message (Error "invalid copy"))
end
end
| Get_file_contents f ->
read_and_send f
| Save_file_req (name, text) ->
......@@ -1370,7 +1404,7 @@ end
| Interrupt_req -> C.interrupt ()
| Command_req (nid, cmd) ->
begin
let snid = try Some(any_from_node_ID nid) with Not_found -> None in
let snid = any_from_node_ID nid in
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) -> apply_transform nid s args
| Query s -> P.notify (Message (Query_Info (nid, s)))
......@@ -1387,6 +1421,9 @@ end
let d = get_server_data () in
let s = d.cont.controller_session in
let any = any_from_node_ID nid in
begin match any with
| None -> P.notify (Message (Error "Please select a node id"))
| Some any ->
let focus_on =
match any with
| APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
......@@ -1394,6 +1431,7 @@ end
in
focused_node := Focus_on [focus_on];
reset_and_send_the_whole_tree ()
end
| Unfocus_req -> unfocus ()
| Help_message s -> P.notify (Message (Information s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment