Commit b7a803eb authored by Sylvain Dailler's avatar Sylvain Dailler

Adding Mark_obsolete request. Added constructor Obsolete to update_info.

parent f87661d9
......@@ -1031,6 +1031,13 @@ let remove_item: GMenu.menu_item =
| [r] -> let id = get_node_id r#iter in send_request (Remove_subtree id)
| _ -> print_message "Select only one node to perform this action")
let mark_obsolete_item: GMenu.menu_item =
file_factory#add_item "Mark obsolete"
~callback:(fun () ->
match get_selected_row_references () with
| [r] -> let id = get_node_id r#iter in send_request (Mark_obsolete_req id)
| _ -> print_message "Select only one node to perform this action")
(*************************************)
(* Commands of the Experimental menu *)
(*************************************)
......@@ -1214,6 +1221,12 @@ let treat_notification n =
Hint.replace node_id_pa id (pa, obs, l);
goals_model#set ~row:r#iter ~column:status_column
(image_of_pa_status ~obsolete:obs pa)
| Obsolete b ->
let r = get_node_row id in
let (pa, _obs, l) = Hint.find node_id_pa id in
Hint.replace node_id_pa id (pa, b, l);
goals_model#set ~row:r#iter ~column:status_column
(image_of_pa_status ~obsolete:b pa)
end
| Next_Unproven_Node_Id (asked_id, next_unproved_id) ->
if_selected_alone asked_id
......
......@@ -709,6 +709,19 @@ let clean_session c ~remove ~node_change =
remove_subtree c ~removed:remove ~node_change (APa paid))
(get_proof_attempt_ids s pnid)) s
let mark_as_obsolete ~node_change ~node_obsolete c any =
let s = c.controller_session in
match any with
| APa n ->
let parent = get_proof_attempt_parent s n in
Session_itp.mark_obsolete s n;
node_obsolete any true;
let b = reload_goal_proof_state c parent in
node_change (APn parent) b;
update_proof_node node_change c parent b
| _ -> ()
exception BadCopyPaste
(* Reproduce the transformation made on node on an other one *)
......
......@@ -216,6 +216,11 @@ val clean_session:
node_change:(any -> bool -> unit) -> unit
(** Remove proof_attempts that are not valid from the session *)
val mark_as_obsolete:
node_change:(any -> bool -> unit) ->
node_obsolete:(any -> bool -> unit) ->
controller -> any -> unit
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
notification:(any -> bool -> unit) ->
......
......@@ -51,6 +51,7 @@ type update_info =
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
| Obsolete of bool
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
......@@ -91,6 +92,7 @@ type ide_request =
| Copy_detached of node_ID
| Save_file_req of string * string
| Get_first_unproven_node of node_ID
| Mark_obsolete_req of node_ID
| Get_Session_Tree_req
| Clean_req
| Save_req
......@@ -104,7 +106,7 @@ let modify_session (r: ide_request) =
match r with
| Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
| Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
| Replay_req | Clean_req -> true
| Replay_req | Clean_req | Mark_obsolete_req _ -> true
| Open_session_req _ | Set_max_tasks_req _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
......
......@@ -57,6 +57,7 @@ type update_info =
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
| Obsolete of bool
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
......@@ -98,6 +99,7 @@ type ide_request =
| Save_file_req of string * string
(* Save_file_req (filename, content_of_file). Save the file *)
| Get_first_unproven_node of node_ID
| Mark_obsolete_req of node_ID
| Get_Session_Tree_req
| Clean_req
| Save_req
......
......@@ -258,6 +258,7 @@ let print_request fmt r =
| Copy_detached _ -> fprintf fmt "copy detached"
| Get_Session_Tree_req -> fprintf fmt "get session tree"
| Save_file_req _ -> fprintf fmt "save file"
| Mark_obsolete_req _ -> fprintf fmt "mark obsolete"
| Clean_req -> fprintf fmt "clean"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
......@@ -983,6 +984,18 @@ let () =
(* TODO make replay print *)
C.replay ~use_steps:false d.cont ~callback:callback ~remove_obsolete:false
(* ---------------- Mark obsolete ------------------ *)
let mark_obsolete n =
let d = get_server_data () in
let any = any_from_node_ID n in
let node_change x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Proved b)) in
let node_obsolete x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Obsolete b)) in
C.mark_as_obsolete ~node_obsolete ~node_change d.cont any
(* ----------------- locate next unproven node -------------------- *)
let notify_first_unproven_node d ni =
......@@ -1064,6 +1077,7 @@ let () =
C.copy_detached ~copy d.cont from_any
| Get_file_contents f ->
read_and_send f
| Mark_obsolete_req n -> mark_obsolete n
| Save_file_req (name, text) ->
save_file name text;
| Get_task nid -> send_task nid
......
......@@ -82,6 +82,9 @@ let convert_update u =
"proof_attempt", convert_proof_attempt pas;
"obsolete", Bool b;
"limit", convert_limit l]
| Obsolete b ->
Obj ["update_info", String "Obsolete";
"obsolete", Bool b]
let convert_notification_constructor n =
match n with
......@@ -125,6 +128,7 @@ let convert_request_constructor (r: ide_request) =
| Copy_detached _ -> String "Copy_detached"
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Get_Session_Tree_req -> String "Get_Session_Tree_req"
| Mark_obsolete_req _ -> String "Mark_obsolete_req"
| Clean_req -> String "Clean_req"
| Save_req -> String "Save_req"
| Reload_req -> String "Reload_req"
......@@ -186,6 +190,9 @@ let print_request_to_json (r: ide_request): Json_base.value =
"node_ID", Int id]
| Get_Session_Tree_req ->
Obj ["ide_request", cc r]
| Mark_obsolete_req n ->
Obj ["ide_request", cc r;
"node_ID", Int n]
| Clean_req ->
Obj ["ide_request", cc r]
| Save_req ->
......@@ -374,6 +381,8 @@ let parse_request (constr: string) l =
Copy_detached n
| "Get_Session_Tree_req", [] ->
Get_Session_Tree_req
| "Mark_obsolete_req", ["node_ID", Int n] ->
Mark_obsolete_req n
| "Clean_req" , [] ->
Clean_req
| "Save_req", [] ->
......@@ -483,6 +492,9 @@ let parse_update j =
"obsolete", Bool b;
"limit", l] ->
Proof_status_change (parse_proof_attempt pas, b, parse_limit_from_json l)
| Obj ["update_info", String "Obsolete";
"obsolete", Bool b] ->
Obsolete b
| _ -> raise NotUpdate
exception NotInfos
......
......@@ -297,6 +297,10 @@ let remove_proof_attempt_pa s (id: proofAttemptID) =
let prover = pa.prover in
remove_proof_attempt s pn prover
let mark_obsolete s (id: proofAttemptID) =
let pa = get_proof_attempt_node s id in
pa.proof_obsolete <- true
(* Iterations functions on the session tree *)
let rec fold_all_any_of_transn s f acc trid =
......
......@@ -156,6 +156,9 @@ val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
from the session [s] *)
val mark_obsolete: session -> proofAttemptID -> unit
(** [mark_obsolete s id] marks [id] as obsolete in [s] *)
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
......
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