Rich printing of goals.

4 files changed, 28 insertions, 23 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a36..562de4562 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -184,12 +184,13 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
+    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+  in
   let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
     let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
       (List.fold_right Environ.push_named d' env,
-       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =
     Context.fold_named_list_context process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
diff --git a/ide/interface.mli b/ide/interface.mli
index 9d19f1c3c..848fb817d 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -18,9 +18,9 @@ type richpp = Richpp.richpp
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : string list;
+  goal_hyp : richpp list;
   (** List of hypotheses *)
-  goal_ccl : string;
+  goal_ccl : richpp;
   (** Goal conclusion *)
 }
 
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 6402789ec..148add6e9 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Preferences
+open Ideutils
 
 class type proof_view =
   object
@@ -83,7 +84,8 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = proof#buffer#insert ~tags (hyp ^ "\n") in
+        let () = insert_xml ~tags proof#buffer hyp in
+        proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
       let () = proof#buffer#insert head_str in
@@ -96,13 +98,14 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        proof#buffer#insert ~tags cur_goal;
+        insert_xml proof#buffer cur_goal;
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        proof#buffer#insert (g ^ "\n")
+        insert_xml proof#buffer g;
+        proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
 
@@ -116,10 +119,12 @@ let mode_cesar (proof : #GText.view_skel) = function
   | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
       proof#buffer#insert "    *** Declarative Mode ***\n";
       List.iter
-        (fun hyp -> proof#buffer#insert (hyp^"\n"))
+        (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n")
         hyps;
       proof#buffer#insert "______________________________________\n";
-      proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
+      proof#buffer#insert "thesis := \n ";
+      insert_xml proof#buffer cur_goal;
+      proof#buffer#insert "\n";
       ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
 
 let rec flatten = function
@@ -152,8 +157,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
       view#buffer#insert "\nYou need to go back and solve them."
@@ -161,8 +166,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
     | _, _, _, _ ->
@@ -174,8 +179,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iteri iter bg
     end
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911d..8afe1cd56 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20140312"
+let protocol_version = "20150815"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -131,14 +131,14 @@ let to_evar = function
   | _ -> raise Marshal_error
 
 let of_goal g =
-  let hyp = of_list of_string g.goal_hyp in
-  let ccl = of_string g.goal_ccl in
+  let hyp = of_list Richpp.of_richpp g.goal_hyp in
+  let ccl = Richpp.of_richpp g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
 let to_goal = function
   | Element ("goal", [], [id; hyp; ccl]) ->
-    let hyp = to_list to_string hyp in
-    let ccl = to_string ccl in
+    let hyp = to_list Richpp.to_richpp hyp in
+    let ccl = Richpp.to_richpp ccl in
     let id = to_string id in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | _ -> raise Marshal_error
@@ -318,10 +318,9 @@ end = struct
               (List.length lg + List.length rg) pr_focus l in
         Printf.sprintf "Still focussed: [%a]." pr_focus g.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 Richpp.raw_print hyps) ^ " |- " ^
+            Richpp.raw_print goal ^ "]" in
       String.concat " " (List.map pr_goal g.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =