Cleaned up a bit goal handling in Coqtop interface. Now we have two queries : goal description, with focused and unfocused goals, and list of currently declared evars.

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

1 files changed, 23 insertions, 17 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index ddfc721e90..3c3324cb97 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -107,25 +107,31 @@ 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 display mode (view:GText.view) goals hints =
-  view#buffer#set_text "";
+let display mode (view:GText.view) goals hints evars =
+  let () = view#buffer#set_text "" in
   match goals with
-    | Interface.No_current_proof -> ()
-    | Interface.Proof_completed ->
-      view#buffer#insert "Proof Completed."
-    | Interface.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.Interface.goal_ccl in
-        view#buffer#insert msg
-      in
-      List.iter iter l
-    | Interface.Uninstantiated_evars el ->
+  | 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 <> [] ->
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
-        let msg = Printf.sprintf "%s\n" evar in
+        let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter el
-    | Interface.Goals g ->
-      mode view g hints
+      List.iter iter evs
+    | _ ->
+      view#buffer#insert "Proof Completed."
+    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 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