Fixing goal display when still focussing but no more goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15622 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 22 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 12cb8c815a..c483bb03e3 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -109,38 +109,39 @@ let mode_cesar (proof:GText.view) = function
       proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
       ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
 
+let rec flatten = function
+| [] -> []
+| (lg, rg) :: l ->
+  let inner = flatten l in
+  List.rev_append lg inner @ rg
+
 let display mode (view:GText.view) goals hints evars =
   let () = view#buffer#set_text "" in
   match goals with
   | None -> ()
     (* No proof in progress *)
-  | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
-    (* A proof has been finished, but not concluded *)
-    begin match evars with
-    | Some evs when evs <> [] ->
+  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+    let bg = flatten (List.rev bg) in
+    let evars = match evars with None -> [] | Some evs -> evs in
+    begin match (bg, evars) with
+    | [], [] ->
+      view#buffer#insert "No more subgoals."
+    | [], _ :: _ ->
+      (* A proof has been finished, but not concluded *)
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evs
-    | _ ->
-      view#buffer#insert "No more subgoals."
+      List.iter iter evars
+    | _, _ ->
+      (* No foreground proofs, but still unfocused ones *)
+      view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+      let iter goal =
+        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+        view#buffer#insert msg
+      in
+      List.iter iter bg
     end
-  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
-    (* No foreground proofs, but still unfocused ones *)
-    view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
-    let rec flatten = function
-    | [] -> []
-    | (lg, rg) :: l ->
-      let inner = flatten l in
-      List.rev_append lg inner @ rg
-    in
-    let bg = flatten (List.rev bg) in
-    let iter goal =
-      let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-      view#buffer#insert msg
-    in
-    List.iter iter bg
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints