Adding rich printing primitives.

8 files changed, 80 insertions, 4 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index e97a2ecee..6a7c2e819 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 88a8486f4..25cb89be3 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 1fb30e4d7..ea4c41ff0 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 464e851f6..9d19f1c3c 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 = {
diff --git a/lib/richpp.ml b/lib/richpp.ml
index c4a9c39d5..fff989ce0 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,38 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
   in
   node xml
 
+type richpp = xml
 
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+  let annotate t = match Pp.Tag.prj t Ppstyle.tag with
+  | None -> None
+  | Some key -> Some (Ppstyle.repr key)
+  in
+  let rec drop = function
+  | PCData s -> [PCData s]
+  | Element (_, annotation, cs) ->
+    let cs = List.concat (List.map drop cs) in
+    match annotation.annotation with
+    | None -> cs
+    | Some s -> [Element (String.concat "." s, [], cs)]
+  in
+  let xml = rich_pp annotate pp in
+  Element ("_", [], drop xml)
+
+let raw_print xml =
+  let buf = Buffer.create 1024 in
+  let rec print = function
+  | PCData s -> Buffer.add_string buf s
+  | Element (_, _, cs) -> List.iter print cs
+  in
+  let () = print xml in
+  Buffer.contents buf
+
+let of_richpp x = Element ("richpp", [], [x])
+let to_richpp xml = match xml with
+| Element ("richpp", [], [x]) -> x
+| _ -> raise Serialize.Marshal_error
diff --git a/lib/richpp.mli b/lib/richpp.mli
index a0d3c374b..7e4b58c9a 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -39,3 +39,29 @@ val xml_of_rich_pp :
   ('annotation -> (string * string) list) ->
   'annotation located Xml_datatype.gxml ->
   Xml_datatype.xml
+
+(** {5 Enriched text} *)
+
+type richpp
+(** Type of text with style annotations *)
+
+val richpp_of_pp : Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
+
+val richpp_of_xml : Xml_datatype.xml -> richpp
+(** Do not use outside of dedicated areas *)
+
+val richpp_of_string : string -> richpp
+(** Make a styled text out of a normal string *)
+
+val repr : richpp -> Xml_datatype.xml
+(** Observe the styled text as XML *)
+
+(** {5 Serialization} *)
+
+val of_richpp : richpp -> Xml_datatype.xml
+val to_richpp : Xml_datatype.xml -> richpp
+
+(** Represent the semi-structured document as a string, dropping any additional
+    information. *)
+val raw_print : richpp -> string
diff --git a/lib/serialize.ml b/lib/serialize.ml
index aa2e3f02a..b14bfb283 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -114,3 +114,7 @@ let to_loc xml =
       with Not_found | Invalid_argument _ -> raise Marshal_error)
   | _ -> raise Marshal_error
 
+let of_xml x = Element ("xml", [], [x])
+let to_xml xml = match xml with
+| Element ("xml", [], [x]) -> x
+| _ -> raise Marshal_error
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 34d3e054c..f4eac5a6b 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -35,3 +35,5 @@ val of_edit_id: int -> xml
 val to_edit_id: xml -> int
 val of_loc : Loc.t -> xml
 val to_loc : xml -> Loc.t
+val of_xml : xml -> xml
+val to_xml : xml -> xml