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

4 files changed, 44 insertions, 27 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index adc766e331..d5fc90e1ee 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -247,3 +247,7 @@ end
 let goals coqtop =
   let () = PrintOpt.enforce_hack coqtop in
   eval_call coqtop Ide_intf.goals
+
+let evars coqtop =
+  let () = PrintOpt.enforce_hack coqtop in
+  eval_call coqtop Ide_intf.evars
diff --git a/ide/coq.mli b/ide/coq.mli
index 5b58113928..662c6ccf2f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -49,7 +49,8 @@ val interp :
   coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
 val rewind : coqtop -> int -> int Interface.value
 val status : coqtop -> Interface.status Interface.value
-val goals : coqtop -> Interface.goals Interface.value
+val goals : coqtop -> Interface.goals option Interface.value
+val evars : coqtop -> Interface.evar list option Interface.value
 val hints : coqtop -> (Interface.hint list * Interface.hint) option Interface.value
 val inloadpath : coqtop -> string -> bool Interface.value
 val mkcases : coqtop -> string -> string list list Interface.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2c6e96218b..7a1d184856 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -825,17 +825,23 @@ object(self)
         else
           (fun _ _ -> ()) in
       try
-        match Coq.goals !mycoqtop with
-          | Interface.Fail (l,str) ->
+        begin match Coq.goals !mycoqtop with
+          | Interface.Fail (l, str) ->
             self#set_message ("Error in coqtop :\n"^str)
           | Interface.Good goals ->
-            let hints = match Coq.hints !mycoqtop with
-            | Interface.Fail (_, _) -> None
-            | Interface.Good hints -> hints
-            in
-            Ideproof.display
-              (Ideproof.mode_tactic menu_callback)
-              proof_view goals hints
+            begin match Coq.evars !mycoqtop with
+            | Interface.Fail (l, str) ->
+              self#set_message ("Error in coqtop :\n"^str)
+            | Interface.Good evs ->
+              let hints = match Coq.hints !mycoqtop with
+              | Interface.Fail (_, _) -> None
+              | Interface.Good hints -> hints
+              in
+              Ideproof.display
+                (Ideproof.mode_tactic menu_callback)
+                proof_view goals hints evs
+            end
+        end
       with
         | e -> prerr_endline (Printexc.to_string e)
     end
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