From f4584f8a332c9077844e227c8b86d3cb1daf8b12 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 14 Sep 2015 16:40:28 +0200
Subject: Adding rich printing primitives.

---
 ide/coqOps.ml     | 8 ++++++++
 ide/ideutils.ml   | 6 ++----
 ide/ideutils.mli  | 3 +++
 ide/interface.mli | 1 +
 4 files changed, 14 insertions(+), 4 deletions(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index e97a2eceef..6a7c2e8195 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -164,6 +164,14 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
+let validate s =
+  let open Xml_datatype in
+  let rec validate = function
+  | PCData s -> Glib.Utf8.validate s
+  | Element (_, _, children) -> List.for_all validate children
+  in
+  validate (Richpp.repr s)
+
 module Doc = Document
 
 class coqops
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 88a8486f47..25cb89be3c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,11 +37,9 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
-module StringMap = Map.Make(String)
-
 let translate s = s
 
-let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml =
+let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
   let open Xml_datatype in
   let tag name =
     let name = translate name in
@@ -55,7 +53,7 @@ let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml =
     let tags = try tag t :: tags with Not_found -> tags in
     List.iter (fun xml -> insert tags xml) children
   in
-  insert tags xml
+  insert tags (Richpp.repr msg)
 
 let set_location = ref  (function s -> failwith "not ready")
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1fb30e4d72..ea4c41ff0a 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,6 +52,9 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
+val insert_xml : ?tags:GText.tag list ->
+  #GText.buffer_skel -> Richpp.richpp -> unit
+
 val set_location : (string -> unit) ref
 
 (* In win32, when a command-line is to be executed via cmd.exe
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..9d19f1c3c5 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -12,6 +12,7 @@
 
 type raw = bool
 type verbose = bool
+type richpp = Richpp.richpp
 
 (** The type of coqtop goals *)
 type goal = {
-- 
cgit v1.2.3