diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-14 16:40:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-20 15:20:32 +0200 |
| commit | f4584f8a332c9077844e227c8b86d3cb1daf8b12 (patch) | |
| tree | 8f09f14d3a3273ccdbd7ec86146b70bce5623278 /ide/ideutils.ml | |
| parent | 481d2b681463d2758fec6b2417631491be69f216 (diff) | |
Adding rich printing primitives.
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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") |