From aa0ad1713b109da690f9a56358df1f5ba56c65e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 28 Aug 2016 23:02:23 +0200 Subject: Fix inefficiency in CoqIDE display of tagged text. The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function. --- ide/ideutils.ml | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fe69be9e4..ae668ae8a 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,23 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let translate s = s +let insert_with_tags (buf : #GText.buffer_skel) mark tags text = + (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) + if CList.is_empty tags then buf#insert text + else + let it = buf#get_iter_at_mark `INSERT in + let () = buf#move_mark (`MARK mark) ~where:it in + let () = buf#insert text in + let start = buf#get_iter_at_mark `INSERT in + let stop = buf#get_iter_at_mark (`MARK mark) in + let iter tag = buf#apply_tag tag start stop in + List.iter iter tags let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = 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 mark = buf#create_mark buf#start_iter in let rec insert tags = function - | PCData s -> buf#insert ~tags:(List.rev tags) s + | PCData s -> insert_with_tags buf mark 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 (Richpp.repr msg) + let () = try insert tags (Richpp.repr msg) with _ -> () in + buf#delete_mark (`MARK mark) let set_location = ref (function s -> failwith "not ready") -- cgit v1.2.3