diff --git a/CHANGES.md b/CHANGES.md index 44304b1af69974d1d25dc3416b95758fa91a92f3..47d689f24d6f17517abf8cef36a46ae0b905a6cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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 -------------------------------- diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 879d4cf300d241606ad007042906d161b190c21c..993a579fe64387861b6e4fe7dd83b48193796a2a 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -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 = diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index f4c9141a6c32b0dafa1ef9bf5d68ae336e2e010e..32aed5762070ef95cd19253dc0193c9df383dcc4 100644 --- a/src/ide/gconfig.mli +++ b/src/ide/gconfig.mli @@ -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; diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index 8ceb2e2d9bac846e596b4d284986d21d46c16da6..da280b777d6033f85b95893d67a6d7137036f829 100644 --- a/src/ide/why3ide.ml +++ b/src/ide/why3ide.ml @@ -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 *)