automatically collapse proven goals and move to nearest unproven goal when a goal is proven

src/ide/why3ide.ml

@@ -166,7 +166,7 @@ let (_ : GtkSignal.id) = main_window#connect#destroy
 
 let (_ : GMenu.menu_item) =
   file_factory#add_item ~key:GdkKeysyms._S "_Save session"
-    ~callback:(fun () -> Session_itp.save_session cont.Controller_itp.controller_session)
+    ~callback:(fun () -> Session_itp.save_session cont.controller_session)
 
 let (replay_menu_item : GMenu.menu_item) =
   file_factory#add_item ~key:GdkKeysyms._R "_Replay all"
@@ -343,7 +343,7 @@ let init_comp cont =
   (* add provers *)
   Whyconf.Hprover.iter
       (fun p _ -> add_completion_entry (p.Whyconf.prover_name^","^p.Whyconf.prover_version))
-      cont.Controller_itp.controller_provers;
+      cont.controller_provers;
 
   add_completion_entry "auto";
   add_completion_entry "auto 2";
@@ -677,11 +677,9 @@ let match_transformation_exception (e: exn) =
 
 let move_current_row_selection_up () =
   let current_view = List.hd (goals_view#selection#get_selected_rows) in
-  let current_row = goals_model#get_row_reference current_view in
-  begin match goals_model#iter_parent current_row#iter with
-    | Some parent_iter -> goals_view#selection#select_iter parent_iter
-    | None -> ()
-  end
+  ignore (GTree.Path.up current_view);
+  let row_up = goals_model#get_row_reference current_view in
+  goals_view#selection#select_iter row_up#iter
 
 let move_current_row_selection_down () =
   let current_iter =
@@ -749,6 +747,12 @@ let callback_update_tree_proof cont panid pa_status =
     | Some iter -> update_status_column_from_iter cont iter
     | None -> ()
     end;
+    begin match get_first_unproven_goal_around_pn_in_th cont pa.parent with
+    | Some next_pn ->
+      goals_view#selection#select_iter (row_from_pn next_pn)#iter
+    | None -> ()
+    end;
+    collapse_proven_goals ();
     r
   | _  -> row_from_pan panid (* TODO ? *)
   in

src/session/session_user_interface.ml

 
 open Format
 open Session_itp
+open Controller_itp
 
 (* TODO: raise exceptions instead of using explicit eprintf/exit *)
 let cont_from_files spec usage_str env files provers =
@@ -54,9 +55,66 @@ let cont_from_files spec usage_str env files provers =
   (* return the controller *)
   c
 
-(*********************)
-(* Terminal historic *)
-(*********************)
+(**********************************)
+(* list unproven goal and related *)
+(**********************************)
+
+let rec unproven_goals_below_tn cont acc tn =
+  if tn_proved cont tn then
+    acc                         (* we ignore "dead" goals *)
+  else
+    let sub_tasks = get_sub_tasks cont.controller_session tn in
+    List.fold_left (unproven_goals_below_pn cont) acc sub_tasks
+
+(* note that if goal is not proved and there is no transformation goal
+   is returned *)
+and unproven_goals_below_pn cont acc goal =
+  if pn_proved cont goal then
+    acc                         (* we ignore "dead" transformations *)
+  else
+    match get_transformations cont.controller_session goal with
+    | [] -> goal :: acc
+    | tns -> List.fold_left (unproven_goals_below_tn cont) acc tns
+
+let unproven_goals_below_th cont acc th =
+  if th_proved cont th then
+    acc
+  else
+    let goals = theory_goals th in
+    List.fold_left (unproven_goals_below_pn cont) acc goals
+
+let unproven_goals_below_file cont file =
+  if file_proved cont file then
+    []
+  else
+    let theories = file.file_theories in
+    List.fold_left (unproven_goals_below_th cont) [] theories
+
+let unproven_goals_in_session cont =
+  let files = get_files cont.controller_session in
+  Stdlib.Hstr.fold (fun _key file acc ->
+      let file_goals = unproven_goals_below_file cont file in
+      List.rev_append file_goals acc)
+    files []
+
+let get_first_unproven_goal_around_pn_in_th cont pn =
+  let ses = cont.controller_session in
+  let rec look_around pn =
+    match get_proof_parent ses pn with
+    | Trans tn  ->
+      begin match unproven_goals_below_tn cont [] tn with
+        | [] -> look_around (get_trans_parent ses tn)
+        | l  -> l
+      end
+    | Theory th -> unproven_goals_below_th cont [] th
+  in
+  match look_around pn with
+  | [] -> None
+  | l -> Some (List.hd (List.rev l))
+
+(********************)
+(* Terminal history *)
+(********************)
 
 module type Historic_type = sig
   type historic