diff options
| author | Pierre-Marie Pédrot | 2015-09-14 16:40:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-20 15:20:32 +0200 |
| commit | f4584f8a332c9077844e227c8b86d3cb1daf8b12 (patch) | |
| tree | 8f09f14d3a3273ccdbd7ec86146b70bce5623278 /ide | |
| parent | 481d2b681463d2758fec6b2417631491be69f216 (diff) | |
Adding rich printing primitives.
Diffstat (limited to 'ide')
| -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 |
4 files changed, 14 insertions, 4 deletions
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 = { |