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

4 files changed, 73 insertions, 42 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
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 6abea2ad8..18a602af2 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -20,7 +20,10 @@ type goal = {
 }
 
 type goals =
-  | Message of string
+  | No_current_proof
+  | Proof_completed
+  | Unfocused_goals of goal list
+  | Uninstantiated_evars of string list
   | Goals of goal list
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
@@ -210,14 +213,31 @@ let to_goal = function
 | _ -> raise Marshal_error
 
 let of_goals = function
-| Message s ->
-  Element ("goals", ["val", "message"], [PCData s])
+| No_current_proof ->
+  Element ("goals", ["val", "no_current_proof"], [])
+| Proof_completed ->
+  Element ("goals", ["val", "proof_completed"], [])
+| Unfocused_goals l ->
+  let xml = of_list of_goal l in
+  Element ("goals", ["val", "unfocused_goals"], [xml])
+| Uninstantiated_evars el ->
+  let xml = of_list of_string el in
+  Element ("goals", ["val", "uninstantiated_evars"], [xml])
 | Goals l ->
   let xml = of_list of_goal l in
   Element ("goals", ["val", "goals"], [xml])
 
 let to_goals = function
-| Element ("goals", ["val", "message"], l) -> Message (raw_string l)
+| Element ("goals", ["val", "no_current_proof"], []) ->
+  No_current_proof
+| Element ("goals", ["val", "proof_completed"], []) ->
+  Proof_completed
+| Element ("goals", ["val", "unfocused_goals"], [xml]) ->
+  let l = to_list to_goal xml in
+  Unfocused_goals l
+| Element ("goals", ["val", "uninstantiated_evars"], [xml]) ->
+  let l = to_list to_string xml in
+  Uninstantiated_evars l
 | Element ("goals", ["val", "goals"], [xml]) ->
   let l = to_list to_goal xml in
   Goals l
@@ -276,7 +296,10 @@ let pr_mkcases l =
   "[" ^ String.concat " | " l ^ "]"
 
 let pr_goals = function
-| Message s -> "Message: " ^ s
+| No_current_proof -> "No current proof."
+| Proof_completed -> "Proof completed."
+| Unfocused_goals gl -> Printf.sprintf "Still %i unfocused goals." (List.length gl)
+| Uninstantiated_evars el -> Printf.sprintf "Still %i uninstantiated evars." (List.length el)
 | Goals gl ->
   let pr_menu s = s in
   let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 02b852534..3752d0142 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -16,7 +16,10 @@ type goal = {
 }
 
 type goals =
-  | Message of string
+  | No_current_proof
+  | Proof_completed
+  | Unfocused_goals of goal list
+  | Uninstantiated_evars of string list
   | Goals of goal list
 
 type 'a call
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 95a6dcf6a..a276f3292 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -400,6 +400,20 @@ let concl_next_tac sigma concl =
     "right"
   ])
 
+let process_goal sigma g =
+  let env = Goal.V82.env sigma g in
+  let ccl =
+    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
+    string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
+  let process_hyp h_env d acc =
+    let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
+    (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
+(*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
+  let hyps =
+    List.rev (Environ.fold_named_context process_hyp env ~init: []) in
+  { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl }
+(*         hyps,(ccl,concl_next_tac sigma g)) *)
+
 let goals () =
   try
     let pfts =
@@ -408,42 +422,18 @@ let goals () =
   let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
   if all_goals = [] then
     begin
-      Ide_intf.Message (string_of_ppcmds (
-        let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
-        match bgoals with
-          | [] ->
-              let exl = Evarutil.non_instantiated sigma in
-              (str (if exl = [] then "Proof Completed." else
-                      "No more subgoals but non-instantiated existential variables:") ++
-               (fnl ()) ++ (pr_evars_int 1 exl))
-          | _ ->
-              Util.list_fold_left_i
-                (fun i a g ->
-                   a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1
-                (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ()))
-                bgoals))
+      let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
+      if bgoals = [] then
+        let exl = Evarutil.non_instantiated sigma in
+        if exl = [] then Ide_intf.Proof_completed
+        else
+          let el = List.map (fun evar -> string_of_ppcmds (pr_evar evar)) exl in
+          Ide_intf.Uninstantiated_evars el
+      else Ide_intf.Unfocused_goals (List.map (process_goal sigma) bgoals)
     end
   else
-    begin
-      let process_goal g =
-        let env = Goal.V82.env sigma g in
-        let ccl =
-          let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-          string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
-        let process_hyp h_env d acc =
-          let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
-          (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
-(*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
-        let hyps =
-          List.rev (Environ.fold_named_context process_hyp env ~init: []) in
-        { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl }
-(*         hyps,(ccl,concl_next_tac sigma g)) *)
-      in
-      Ide_intf.Goals (List.map process_goal all_goals)
-    end
-  with Proof_global.NoCurrentProof ->
-    Ide_intf.Message "" (* quick hack to have a clean message screen *)
-
+    Ide_intf.Goals (List.map (process_goal sigma) all_goals)
+  with Proof_global.NoCurrentProof -> Ide_intf.No_current_proof
 
 (** Other API calls *)