fix #292

Add an option in the preferences to disallow the automatic jump after a
goal is completed. Jump can still be performed by calling next in command
line.

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
 --------------------------------

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 =

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;

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 *)