From 8b609e4e6df906dc16e8fa506a71046ab3b8f16c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 18:09:48 +0200 Subject: Pluging in tag preferences into buffer printing. --- ide/ideutils.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 053bba805d..88a8486f47 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,7 +37,25 @@ 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 open Xml_datatype in + let tag name = + let name = translate name in + match GtkText.TagTable.lookup buf#tag_table name with + | None -> raise Not_found + | Some tag -> new GText.tag tag + in + let rec insert tags = function + | PCData s -> buf#insert ~tags:(List.rev tags) s + | Element (t, _, children) -> + let tags = try tag t :: tags with Not_found -> tags in + List.iter (fun xml -> insert tags xml) children + in + insert tags xml let set_location = ref (function s -> failwith "not ready") -- cgit v1.2.3 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/ideutils.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'ide/ideutils.ml') 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") -- cgit v1.2.3 From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- ide/ideutils.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 25cb89be3c..2e4adba735 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,6 +37,17 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) +let xml_to_string xml = + let open Xml_datatype in + let buf = Buffer.create 1024 in + let rec iter = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, children) -> + List.iter iter children + in + let () = iter (Richpp.repr xml) in + Buffer.contents buf + let translate s = s let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = @@ -288,7 +299,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Pp.message_level -> string -> unit +type logger = Pp.message_level -> Richpp.richpp -> unit let default_logger level message = let level = match level with @@ -298,7 +309,7 @@ let default_logger level message = | Pp.Warning -> `WARNING | Pp.Error -> `ERROR in - Minilib.log ~level message + Minilib.log ~level (xml_to_string message) (** {6 File operations} *) -- cgit v1.2.3 From 82ac0604888679bc2fbdeda9ac264d7cd10f7928 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:52:33 +0100 Subject: Avoid warnings about loop indices. --- ide/ideutils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 2e4adba735..ffa07ead7e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -31,7 +31,7 @@ let push_info,pop_info,clear_info = let size = ref 0 in (fun s -> incr size; ignore (status_context#push s)), (fun () -> decr size; status_context#pop ()), - (fun () -> for i = 1 to !size do status_context#pop () done; size := 0) + (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0) let flash_info = let flash_context = status#new_context ~name:"Flash" in -- cgit v1.2.3 From 74c29764359272b29af081b30762549777ae8825 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:05:03 +0100 Subject: Remove some useless type declarations. --- ide/ideutils.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ffa07ead7e..51ae76ff54 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -9,8 +9,6 @@ open Preferences -exception Forbidden - let warn_image () = let img = GMisc.image () in img#set_stock `DIALOG_WARNING; -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- ide/ideutils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 5892fb3d96..44a86556a5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*