Adapting the IDE interface with the focussed display.

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

1 files changed, 7 insertions, 0 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 569e503c3b..12cb8c815a 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -130,6 +130,13 @@ let display mode (view:GText.view) goals hints evars =
   | 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