Now Coqtop has a richer way to answer a query about its pending goals. Answers are semantic and not simple strings anymore. Still to be ameliorated.

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

1 files changed, 17 insertions, 2 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 58e7d2734..742ffc46a 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -97,7 +97,22 @@ let mode_cesar (proof:GText.view) = function
 let display mode (view:GText.view) goals =
   view#buffer#set_text "";
   match goals with
-    | Ide_intf.Message msg ->
+    | Ide_intf.No_current_proof -> ()
+    | Ide_intf.Proof_completed ->
+      view#buffer#insert "Proof Completed."
+    | Ide_intf.Unfocused_goals l ->
+      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.Ide_intf.goal_ccl in
         view#buffer#insert msg
+      in
+      List.iter iter l
+    | Ide_intf.Uninstantiated_evars el ->
+      view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
+      let iter evar =
+        let msg = Printf.sprintf "%s\n" evar in
+        view#buffer#insert msg
+      in
+      List.iter iter el
     | Ide_intf.Goals g ->
-        mode view g
+      mode view g