diff options
-rw-r--r-- | ide/coqOps.ml | 8 | ||||
-rw-r--r-- | ide/ideutils.ml | 6 | ||||
-rw-r--r-- | ide/ideutils.mli | 3 | ||||
-rw-r--r-- | ide/interface.mli | 1 | ||||
-rw-r--r-- | lib/richpp.ml | 34 | ||||
-rw-r--r-- | lib/richpp.mli | 26 | ||||
-rw-r--r-- | lib/serialize.ml | 4 | ||||
-rw-r--r-- | lib/serialize.mli | 2 |
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 |