From 899d186714a2bcb2d51902c918d0cb20d1815288 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 10 Jul 2012 13:27:31 +0000
Subject: 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
---
 ide/ideproof.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'ide')

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
-- 
cgit v1.2.3