From 6bb006b9a4e47a28390a670c069d93a03385fcda Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Mon, 30 Jul 2018 16:46:06 +0200
Subject: [PATCH] itp_server: Allow get_first_unproven_goal_around to always
 return a node

This is useful for users of the API who don't know what node they start on
when focusing at start of the interactive process.
---
 src/session/itp_server.ml    |  1 +
 src/session/server_utils.ml  |  4 ++--
 src/session/server_utils.mli | 21 +++++++++++++++------
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 4c6e56d7a..3807e1185 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -1312,6 +1312,7 @@ end
     | Some any ->
       let unproven_any =
         get_first_unproven_goal_around
+          ~always_send:false
           ~proved:(Session_itp.any_proved s)
           ~children:(get_undetached_children_no_pa s)
           ~get_parent:(get_any_parent s)
diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml
index f83083968..4f90c6f86 100644
--- a/src/session/server_utils.ml
+++ b/src/session/server_utils.ml
@@ -485,7 +485,7 @@ let split_list l node =
   split_list l []
 
 let get_first_unproven_goal_around
-    ~proved ~children ~get_parent ~is_goal ~is_pa node =
+    ~always_send ~proved ~children ~get_parent ~is_goal ~is_pa node =
   let rec look_around node =
     match get_parent node with
     | None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
@@ -505,7 +505,7 @@ let get_first_unproven_goal_around
   | [] ->
     begin
       match before_node with
-      | [] -> None
+      | [] -> if always_send then Some node else None
       | hd :: _tl -> Some hd
     end
   | hd :: _tl  -> Some hd
diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli
index ba06b1a88..a44e3dba4 100644
--- a/src/session/server_utils.mli
+++ b/src/session/server_utils.mli
@@ -83,10 +83,19 @@ val interp:
   Controller_itp.controller ->
   Session_itp.any option -> string -> command
 
-
+(* Find the first unproven goal around the node given.
+   @param always_send: if true then always returns something
+   @param proved     : oracle for proved node
+   @param children   : returns the list children of a node
+   @param get_parent : returns the parent of a node
+   @param is_goal    : answer true iff a given node is a goal
+   @param is_pa      : answer true iff a given node is a proof attempt
+   @param node       : node_id
+*)
 val get_first_unproven_goal_around:
-    proved:('a -> bool) ->
-      children:('a -> 'a list) ->
-        get_parent:('a -> 'a option) ->
-          is_goal:('a -> bool) ->
-            is_pa:('a -> bool) -> 'a -> 'a option
+    always_send:bool ->
+      proved:('a -> bool) ->
+        children:('a -> 'a list) ->
+          get_parent:('a -> 'a option) ->
+            is_goal:('a -> bool) ->
+              is_pa:('a -> bool) -> 'a -> 'a option
-- 
GitLab