STM: report the (structured) goals as XML

The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.

4 files changed, 52 insertions, 9 deletions

diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index cd20d7a5c1..812a6298ac 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -145,10 +145,10 @@ let to_goal = function
 
 let of_goals g =
   let of_glist = of_list of_goal in
-  let fg = of_list of_goal g.fg_goals in
-  let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
-  let shelf = of_list of_goal g.shelved_goals in
-  let given_up = of_list of_goal g.given_up_goals in
+  let fg = of_list of_goal g.Proof.fg_goals in
+  let bg = of_list (of_pair of_glist of_glist) g.Proof.bg_goals in
+  let shelf = of_list of_goal g.Proof.shelved_goals in
+  let given_up = of_list of_goal g.Proof.given_up_goals in
   Element ("goals", [], [fg; bg; shelf; given_up])
 let to_goals = function
   | Element ("goals", [], [fg; bg; shelf; given_up]) ->
@@ -157,7 +157,8 @@ let to_goals = function
     let bg = to_list (to_pair to_glist to_glist) bg in
     let shelf = to_list to_goal shelf in
     let given_up = to_list to_goal given_up in
-    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up }
+    { Proof.fg_goals = fg; bg_goals = bg; shelved_goals = shelf; 
+      given_up_goals = given_up }
   | _ -> raise Marshal_error
 
 let of_coq_info info =
@@ -306,8 +307,8 @@ end = struct
   let pr_int i = string_of_int i
   let pr_bool b = Printf.sprintf "%B" b
   let pr_goal (g : goals) =
-    if g.fg_goals = [] then
-      if g.bg_goals = [] then "Proof completed."
+    if g.Proof.fg_goals = [] then
+      if g.Proof.bg_goals = [] then "Proof completed."
       else
         let rec pr_focus _ = function
           | [] -> assert false
@@ -315,13 +316,13 @@ end = struct
           | (lg, rg) :: l ->
             Printf.sprintf "%i:%a"
               (List.length lg + List.length rg) pr_focus l in
-        Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+        Printf.sprintf "Still focussed: [%a]." pr_focus g.Proof.bg_goals
     else
       let pr_menu s = s in
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
         "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
             pr_menu goal ^ "]" in
-      String.concat " " (List.map pr_goal g.fg_goals)
+      String.concat " " (List.map pr_goal g.Proof.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =
     let path =
diff --git a/lib/feedback.ml b/lib/feedback.ml
index e01844a482..14a1861e8b 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -68,6 +68,7 @@ type feedback_content =
   | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
+  | StructuredGoals of Loc.t * xml
   | FileLoaded of string * string
   | Message of message
 
@@ -93,6 +94,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
        let n, s = to_pair to_string to_string ns in
        SlaveStatus(n,s)
   | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
+  | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x)
   | "fileloaded", [dirpath; filename] ->
        FileLoaded(to_string dirpath, to_string filename)
   | "message", [m] -> Message (to_message m)
@@ -124,6 +126,8 @@ let of_feedback_content = function
         [of_pair of_string of_string (n,s)]
   | Goals (loc,s) ->
       constructor "feedback_content" "goals" [of_loc loc;of_string s]
+  | StructuredGoals (loc, x) ->
+      constructor "feedback_content" "structuredgoals" [of_loc loc; x]
   | FileLoaded(dirpath, filename) ->
       constructor "feedback_content" "fileloaded" [
         of_string dirpath;
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 7e7b57625f..775f71e9e5 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -43,6 +43,7 @@ type feedback_content =
   | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
+  | StructuredGoals of Loc.t * xml
   | FileLoaded of string * string
   | Message of message
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e837de0ce3..3e8181fe93 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -503,6 +503,24 @@ end = struct
 
 end
 
+
+(* TODO: Might not be the right place for this *)
+(* TODO: Currently, this mimics the process_goal function of ide/ide_slave.ml, 
+ * but we have the opportunity to provide more structure in the xml, here. *)
+let process_goal sigma g =
+  let env = Goal.V82.env sigma g in
+  let id = Goal.uid g in
+  let ccl =
+    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
+    let ccl_string = string_of_ppcmds (Printer.pr_goal_concl_style_env env sigma norm_constr) in
+    Xml_datatype.Element ("conclusion", [], [Xml_datatype.PCData ccl_string]) in
+  let process_hyp env h_env acc =
+    let hyp_string = (string_of_ppcmds (Printer.pr_var_decl env sigma h_env)) in
+    (Xml_datatype.Element ("hypothesis", [], [Xml_datatype.PCData hyp_string])) :: acc in
+  let hyps = Xml_datatype.Element ("hypotheses", [], 
+    (List.rev (Environ.fold_named_context process_hyp env ~init:[]))) in
+  Xml_datatype.Element ("goal", [("id", id)], [hyps; ccl])
+
 let print_goals_of_state, forward_feedback =
   let already_printed = ref Stateid.Set.empty in
   let add_to_already_printed =
@@ -517,6 +535,25 @@ let print_goals_of_state, forward_feedback =
       add_to_already_printed id;
       try
         Option.iter (fun { proof = pstate } ->
+          let pfts = Proof_global.proof_of_state pstate in
+          let structured_goals = Proof.map_structured_proof pfts process_goal in
+          let xml_bg_goal = fun (l, r) -> Xml_datatype.Element("bg_goal", [], 
+              [Xml_datatype.Element("left_bg_goals", [], l); 
+               Xml_datatype.Element("right_bg_goals", [], r)]) in
+
+          let xml_structured_goals = Xml_datatype.Element("goals", [],
+            [ Xml_datatype.Element("focussed_goals", [], 
+                structured_goals.Proof.fg_goals);
+              Xml_datatype.Element("bg_goals", [], 
+                List.map xml_bg_goal structured_goals.Proof.bg_goals);
+              Xml_datatype.Element("shelved_goals", [], 
+                structured_goals.Proof.shelved_goals);
+              Xml_datatype.Element("given_up_goals", [], 
+                structured_goals.Proof.given_up_goals)
+            ]
+          ) in
+          Pp.feedback ~state_id:id
+           (Feedback.StructuredGoals (Loc.ghost, xml_structured_goals));
           Pp.feedback ~state_id:id
             (Feedback.Goals
               (Loc.ghost, Pp.string_of_ppcmds