Commit 8e49dc02 authored by Andrei Paskevich's avatar Andrei Paskevich

several modifications in Session and IDE

- provide a method to mark proof attempts as obsolete
  (thus, we can replay a saved tree even if the source
  file hasn't changed)
- cleaning applies to a subtree (like transformations
  and provers), not only at the first level
- obsolete proof attempts do not count as successuful
parent b989b344
......@@ -197,6 +197,7 @@ let iconname_prover = "wizard32"
let iconname_transf = "configure32"
let iconname_editor = "edit32"
let iconname_replay = "refresh32"
let iconname_cancel = "cut32"
let iconname_reload = "movefile32"
let iconname_remove = "deletefile32"
let iconname_cleaning = "trashb32"
......@@ -223,6 +224,7 @@ let image_prover = ref !image_default
let image_transf = ref !image_default
let image_editor = ref !image_default
let image_replay = ref !image_default
let image_cancel = ref !image_default
let image_reload = ref !image_default
let image_remove = ref !image_default
let image_cleaning = ref !image_default
......@@ -250,6 +252,7 @@ let resize_images size =
image_transf := image ~size iconname_transf;
image_editor := image ~size iconname_editor;
image_replay := image ~size iconname_replay;
image_cancel := image ~size iconname_cancel;
image_reload := image ~size iconname_reload;
image_remove := image ~size iconname_remove;
image_cleaning := image ~size iconname_cleaning;
......
......@@ -66,6 +66,7 @@ val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
val image_editor : GdkPixbuf.pixbuf ref
val image_replay : GdkPixbuf.pixbuf ref
val image_cancel : GdkPixbuf.pixbuf ref
val image_reload : GdkPixbuf.pixbuf ref
val image_remove : GdkPixbuf.pixbuf ref
val image_cleaning : GdkPixbuf.pixbuf ref
......
......@@ -171,7 +171,7 @@ let () =
let b1 = GButton.radio_button
~packing:context_box#add ~label:"Unproved goals" ()
in
b1#misc#set_tooltip_markup "When selected, tools below are applied\nonly on <b>unproved</b> goals";
b1#misc#set_tooltip_markup "When selected, tools below are applied only to <b>unproved</b> goals";
let (_ : GtkSignal.id) =
b1#connect#clicked
~callback:(fun () -> context_unproved_goals_only := true)
......@@ -179,7 +179,7 @@ let () =
let b2 = GButton.radio_button
~group:b1#group ~packing:context_box#add ~label:"All goals" ()
in
b2#misc#set_tooltip_markup "When selected, tools below are applied\nto all goals";
b2#misc#set_tooltip_markup "When selected, tools below are applied to all goals";
let (_ : GtkSignal.id) =
b2#connect#clicked
~callback:(fun () -> context_unproved_goals_only := false)
......@@ -614,6 +614,16 @@ let replay_obsolete_proofs () =
~context_unproved_goals_only:!context_unproved_goals_only a)
(get_selected_row_references ())
(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)
let cancel_proofs () =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
M.cancel a)
(get_selected_row_references ())
(*****************************************************)
......@@ -920,7 +930,8 @@ let () =
()
in
let b = GButton.button ~packing:provers_box#add ~label:n () in
b#misc#set_tooltip_markup "Click to start this prover\non the <b>selected</b> goal(s)";
b#misc#set_tooltip_markup ("Start <tt>" ^ p.Session.prover_name ^
"</tt> on the <b>selected goals</b>");
(* prend de la place pour rien
let i = GMisc.image ~pixbuf:(!image_prover) () in
......@@ -953,7 +964,7 @@ let () =
let () =
let b = GButton.button ~packing:transf_box#add ~label:"Split" () in
b#misc#set_tooltip_markup "Click to apply transformation <tt>split_goal</tt> to the <b>selected goals</b>";
b#misc#set_tooltip_markup "Apply the transformation <tt>split_goal</tt> to the <b>selected goals</b>";
let i = GMisc.image ~pixbuf:(!image_transf) () in
let () = b#set_image i#coerce in
......@@ -964,7 +975,7 @@ let () =
let () =
let b = GButton.button ~packing:transf_box#add ~label:"Inline" () in
b#misc#set_tooltip_markup "Click to apply transformation <tt>inline_goal</tt> to the <b>selected goals</b>";
b#misc#set_tooltip_markup "Apply the transformation <tt>inline_goal</tt> to the <b>selected goals</b>";
let i = GMisc.image ~pixbuf:(!image_transf) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
......@@ -1235,7 +1246,7 @@ let () =
let () =
let b = GButton.button ~packing:tools_box#add ~label:"Edit" () in
b#misc#set_tooltip_markup "Click to edit the <b>selected proof</b>\nwith the appropriate editor";
b#misc#set_tooltip_markup "Edit the <b>selected proof</b> with the appropriate editor";
let i = GMisc.image ~pixbuf:(!image_editor) () in
let () = b#set_image i#coerce in
......@@ -1245,7 +1256,7 @@ let () =
let () =
let b = GButton.button ~packing:tools_box#add ~label:"Replay" () in
b#misc#set_tooltip_markup "Replay all the <b>successful</b> but <b>obsolete</b> proofs below the current selection";
b#misc#set_tooltip_markup "Replay <b>obsolete</b> proofs below the current selection";
let i = GMisc.image ~pixbuf:(!image_replay) () in
let () = b#set_image i#coerce in
......@@ -1253,6 +1264,15 @@ let () =
b#connect#pressed ~callback:replay_obsolete_proofs
in ()
let () =
let b = GButton.button ~packing:tools_box#add ~label:"Cancel" () in
b#misc#set_tooltip_markup "Mark all proofs below the current selection as <b>obsolete</b>";
let i = GMisc.image ~pixbuf:(!image_cancel) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
b#connect#pressed ~callback:cancel_proofs
in ()
(*************)
(* removing *)
......@@ -1294,7 +1314,7 @@ let confirm_remove_selection () =
info_window
~callback:(fun () -> List.iter remove_proof l)
`QUESTION
"Do you really want to remove all the selected proofs?"
"Do you really want to remove the selected proof attempts?"
(*
| _ ->
info_window `INFO "Please select exactly one item to remove"
......@@ -1302,7 +1322,7 @@ let confirm_remove_selection () =
let () =
let b = GButton.button ~packing:cleaning_box#add ~label:"Remove" () in
b#misc#set_tooltip_markup "Removes the selected\n<b>proof</b> or <b>transformation</b>";
b#misc#set_tooltip_markup "Remove selected <b>proof attempts</b> and <b>transformations</b>";
let i = GMisc.image ~pixbuf:(!image_remove) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
......@@ -1315,7 +1335,7 @@ let clean_selection () =
let () =
let b = GButton.button ~packing:cleaning_box#add ~label:"Clean" () in
b#misc#set_tooltip_markup "Removes non successful proof_attempts\nassociated to a proved goal";
b#misc#set_tooltip_markup "Remove unsuccessful <b>proof attempts</b> associated to proved goals";
let i = GMisc.image ~pixbuf:(!image_cleaning) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
......
......@@ -344,6 +344,7 @@ let check_theory_proved t =
let rec check_goal_proved g =
let b1 = Hashtbl.fold
(fun _ a acc -> acc ||
not a.proof_obsolete &&
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid} -> true
| _ -> false) g.external_proofs false
......@@ -790,7 +791,7 @@ let reload_proof obsolete goal pid old_a =
(Undetected_prover pid)
in
let old_res = old_a.proof_state in
let obsolete = obsolete or old_a.proof_obsolete in
let obsolete = obsolete || old_a.proof_obsolete in
(* eprintf "proof_obsolete : %b@." obsolete; *)
let a =
raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
......@@ -1351,6 +1352,32 @@ let replay ~obsolete_only ~context_unproved_goals_only a =
(replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only)
tr.subgoals
(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)
let cancel_proof a = set_proof_state ~obsolete:true a a.proof_state
let rec cancel_goal_or_children g =
Hashtbl.iter (fun _ a -> cancel_proof a) g.external_proofs;
Hashtbl.iter
(fun _ t -> List.iter cancel_goal_or_children t.subgoals)
g.transformations
let cancel a =
match a with
| Goal g ->
cancel_goal_or_children g
| Theory th ->
List.iter cancel_goal_or_children th.goals
| File file ->
List.iter
(fun th -> List.iter cancel_goal_or_children th.goals)
file.theories
| Proof_attempt a ->
cancel_goal_or_children a.proof_goal
| Transformation tr ->
List.iter cancel_goal_or_children tr.subgoals
(*********************************)
(* method: check existing proofs *)
......@@ -1663,7 +1690,9 @@ let rec clean_goal g =
Hashtbl.iter
(fun _ t ->
if not t.transf_proved then
remove_transformation t)
remove_transformation t
else
List.iter clean_goal t.subgoals)
g.transformations
end
else
......
......@@ -240,6 +240,9 @@ module Make(O: OBSERVER) : sig
with result was 'valid'
*)
val cancel : any -> unit
(** [cancel a] marks all proofs under [a] as obsolete *)
type report =
| Wrong_result of Call_provers.prover_result * Call_provers.prover_result
| CallFailed of exn
......
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