Commit b1805227 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_292' into 'master'

fix #292

Closes #292

See merge request !113
parents fb3da6dc 95dc27a6
......@@ -31,6 +31,9 @@ Transformations
Counterexamples
* Improved display of counterexamples in Task view
IDE
* Added a checkbutton in preferences to disallow auto jumping to next unproved
goal
Version 1.2.0, February 11, 2019
--------------------------------
......
......@@ -45,6 +45,7 @@ type t =
mutable max_boxes : int;
mutable allow_source_editing : bool;
mutable saving_policy : int;
mutable auto_next : bool; (* true if auto jump to next goal *)
(** 0 = always, 1 = never, 2 = ask *)
mutable premise_color : string;
mutable neg_premise_color : string;
......@@ -81,6 +82,7 @@ type ide = {
ide_max_boxes : int;
ide_allow_source_editing : bool;
ide_saving_policy : int;
ide_auto_next : bool;
ide_premise_color : string;
ide_neg_premise_color : string;
ide_goal_color : string;
......@@ -108,6 +110,7 @@ let default_ide =
ide_max_boxes = 16;
ide_allow_source_editing = true;
ide_saving_policy = 2;
ide_auto_next = true;
ide_premise_color = "chartreuse";
ide_neg_premise_color = "pink";
ide_goal_color = "gold";
......@@ -152,6 +155,8 @@ let load_ide section =
get_bool section ~default:default_ide.ide_allow_source_editing "allow_source_editing";
ide_saving_policy =
get_int section ~default:default_ide.ide_saving_policy "saving_policy";
ide_auto_next =
get_bool section ~default:default_ide.ide_auto_next "auto_next";
ide_premise_color =
get_string section ~default:default_ide.ide_premise_color
"premise_color";
......@@ -216,6 +221,7 @@ let load_config config original_config =
max_boxes = ide.ide_max_boxes;
allow_source_editing = ide.ide_allow_source_editing ;
saving_policy = ide.ide_saving_policy ;
auto_next = ide.ide_auto_next ;
premise_color = ide.ide_premise_color;
neg_premise_color = ide.ide_neg_premise_color;
goal_color = ide.ide_goal_color;
......@@ -733,6 +739,16 @@ let general_settings (c : t) (notebook:GPack.notebook) =
source_editing_check#connect#toggled ~callback:
(fun () -> c.allow_source_editing <- not c.allow_source_editing)
in
(* Auto jump to next unproved goals *)
let auto_next_check = GButton.check_button
~label:"Allow auto jumping to next unproved goal"
~packing:vb#add ()
~active:c.auto_next
in
let (_: GtkSignal.id) =
auto_next_check#connect#toggled ~callback:
(fun () -> c.auto_next <- not c.auto_next)
in
(* session saving policy *)
let set_saving_policy n () = c.saving_policy <- n in
let saving_policy_frame =
......
......@@ -27,6 +27,7 @@ type t =
mutable max_boxes : int;
mutable allow_source_editing : bool;
mutable saving_policy : int;
mutable auto_next : bool;
mutable premise_color : string;
mutable neg_premise_color : string;
mutable goal_color : string;
......
......@@ -277,6 +277,11 @@ let erase_color_loc (v:GSourceView.source_view) =
(* Elements needed for usage of graphical elements *)
(* Hold the node_id on which "next" was called to allow differentiating on
automatic jump from a user jump *)
let manual_next = ref None
(* [quit_on_saved] set to true by exit function to delay quiting after Saved
notification is received *)
let quit_on_saved = ref false
......@@ -1269,12 +1274,12 @@ let move_current_row_selection_to_next () =
goals_view#set_cursor path view_name_column
| _ -> ()
let move_to_next_unproven_node_id () =
let rows = get_selected_row_references () in
match rows with
| [row] ->
let row_id = get_node_id row#iter in
manual_next := Some row_id;
send_request (Get_first_unproven_node row_id)
| _ -> ()
......@@ -2368,8 +2373,13 @@ let treat_notification n =
| _ -> ()
end
| Next_Unproven_Node_Id (asked_id, next_unproved_id) ->
if is_selected_alone asked_id then
if is_selected_alone asked_id &&
(* The user manually asked for next node from this one *)
(!manual_next = Some asked_id ||
(* or auto next is on *)
gconfig.auto_next) then
begin
manual_next := None;
(* Unselect the potentially selected goal to avoid having two tasks
selected at once when a prover successfully end. To continue the
proof, it is better to only have the new goal selected *)
......
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