Commit 14a9eb14 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_295' into 'master'

ide/session: Add a command that resets all proofs from a session

See merge request !120
parents 17a4fec8 581cddee
......@@ -29,6 +29,8 @@ Transformations
IDE
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
* add a "reset proofs" command in the Tools menu. It removes all proofs in
the session
Realizations
* Added experimental realizations for new Set theories in both Isabelle and
......
......@@ -2140,6 +2140,25 @@ let (_ : GMenu.menu_item) =
~tooltip:"Remove unsuccessful proofs or transformations that are under a proved goal"
~callback
let (_ : GMenu.menu_item) =
(* This is considered risky command so it is intentionally not added to the
context menu. It also trigger the apparition of a popup. *)
let callback () =
let answer =
GToolbox.question_box
~default:2
~title:"Launching unsafe command"
~buttons:["Yes"; "No"]
"Do you really want to remove all proofs from this session ?"
in
match answer with
| 1 -> send_request Reset_proofs_req
| _ -> ()
in
tools_factory#add_item "Reset proofs"
~tooltip:"Remove all proofs attempts or transformations"
~callback
let (_ : GMenu.menu_item) =
let callback =
on_selected_rows ~multiple:true ~notif_kind:"Remove_subtree error" ~action:"remove"
......
......@@ -867,7 +867,26 @@ let clean c ~removed nid =
if do_remove then
remove_subtree ~notification ~removed c any
in
match nid with
| Some nid ->
Session_itp.fold_all_any s clean_aux () nid
| None ->
Session_itp.fold_all_session s clean_aux ()
let reset_proofs c ~removed ~notification nid =
let s = c.controller_session in
(* This function is applied on leafs first for the case of removes *)
let clean_aux () any =
let do_remove =
Session_itp.is_detached s any ||
match any with
| APa _ -> true
| ATn _ -> true
| _ -> false
in
if do_remove then
remove_subtree ~notification ~removed c any
in
match nid with
| Some nid ->
Session_itp.fold_all_any s clean_aux () nid
......
......@@ -283,6 +283,14 @@ val clean: controller -> removed:notifier -> any option -> unit
notifier is called on each removed node.
On None, clean is done on the whole session. *)
val reset_proofs:
controller -> removed:notifier -> notification:notifier ->
any option -> unit
(** Remove each proof attempt or transformation that are below proved
goals. The [removed] notifier is called on each removed node.
On None, clean is done on the whole session. *)
val mark_as_obsolete:
notification:notifier ->
controller -> any option -> unit
......
......@@ -124,6 +124,7 @@ type ide_request =
| Check_need_saving_req
| Exit_req
| Interrupt_req
| Reset_proofs_req
| Get_global_infos
......@@ -151,6 +152,7 @@ let print_request fmt r =
| Check_need_saving_req -> fprintf fmt "check need saving"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
| Reset_proofs_req -> fprintf fmt "reset proofs"
| Get_global_infos -> fprintf fmt "get_global_infos"
let print_msg fmt m =
......
......@@ -142,6 +142,8 @@ type ide_request =
| Check_need_saving_req
| Exit_req
| Interrupt_req
| Reset_proofs_req
(** Remove all proofattempt and transformations even proved ones *)
| Get_global_infos
......
......@@ -1244,6 +1244,9 @@ end
let d = get_server_data () in
C.clean d.cont ~removed nid
let reset_proofs () =
let d = get_server_data () in
C.reset_proofs d.cont ~notification:(notify_change_proved d.cont) ~removed None
let remove_node nid =
let d = get_server_data () in
......@@ -1387,7 +1390,8 @@ end
| Save_req | Check_need_saving_req | Reload_req
| Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req -> true
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req
| Reset_proofs_req -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Remove_subtree nid ->
......@@ -1450,6 +1454,9 @@ end
send_task nid b loc
| Interrupt_req ->
C.interrupt ()
| Reset_proofs_req ->
reset_proofs ();
session_needs_saving := true
| Command_req (nid, cmd) ->
let snid = any_from_node_ID nid in
begin
......
......@@ -174,6 +174,7 @@ let convert_request_constructor (r: ide_request) =
| Reload_req -> String "Reload_req"
| Exit_req -> String "Exit_req"
| Interrupt_req -> String "Interrupt_req"
| Reset_proofs_req -> String "Reset_proofs_req"
| Get_global_infos -> String "Get_global_infos"
open Whyconf
......@@ -229,6 +230,7 @@ let print_request_to_json (r: ide_request): Json_base.json =
| Reload_req
| Exit_req
| Interrupt_req
| Reset_proofs_req
| Get_global_infos ->
convert_record ["ide_request", cc r])
......@@ -506,6 +508,8 @@ let parse_request (constr: string) j =
Save_req
| "Reload_req" ->
Reload_req
| "Reset_proofs_req" ->
Reset_proofs_req
| "Exit_req" ->
Exit_req
| _ -> raise (NotRequest "")
......
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