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') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fe69be9e48..ae668ae8ab 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 From 85790fe5ffc81aaead5961abac820492e2e2c871 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Aug 2016 14:03:21 +0200 Subject: CoqIDE preserves unknown preferences. This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time. --- ide/preferences.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 3241a962dc..64327d74f5 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -33,6 +33,7 @@ type obj = { } let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty +let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty class type ['a] repr = object @@ -617,19 +618,19 @@ let save_pref () = then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in let add = Util.String.Map.add in - let (++) x f = f x in let fold key obj accu = add key (obj.get ()) accu in - - (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++ - Config_lexer.print_file pref_file + let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in + let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in + Config_lexer.print_file pref_file prefs let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in let iter name v = - try (Util.String.Map.find name !preferences).set v - with _ -> () + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m -- cgit v1.2.3 From 58107b74ba65947129aff8203a821d146ecd18ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Aug 2016 14:19:42 +0200 Subject: Fix bug #4421: Messages dialog in Coqide resets. --- ide/coqOps.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 50b3f2c0a0..5b6bad3496 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -785,7 +785,6 @@ object(self) method private handle_failure_aux ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = - messages#clear; messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) -- cgit v1.2.3 From 985e83e60b6665d17b81830aea4fce3384fe2b5a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 20:32:13 +0200 Subject: Fix bug #5051: Large outputs are garbled. Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view. --- ide/ideutils.ml | 22 +++++++++++----------- ide/ideutils.mli | 2 +- ide/wg_MessageView.ml | 9 ++++++--- 3 files changed, 18 insertions(+), 15 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ae668ae8ab..06a1327320 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,37 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let insert_with_tags (buf : #GText.buffer_skel) mark tags text = +let insert_with_tags (buf : #GText.buffer_skel) mark rmark 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 + if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) 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 it = buf#get_iter_at_mark mark in + let () = buf#move_mark rmark ~where:it in + let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in + let start = buf#get_iter_at_mark mark in + let stop = buf#get_iter_at_mark rmark 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 insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = 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 rmark = `MARK (buf#create_mark buf#start_iter) in let rec insert tags = function - | PCData s -> insert_with_tags buf mark tags s + | PCData s -> insert_with_tags buf mark rmark 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 let () = try insert tags (Richpp.repr msg) with _ -> () in - buf#delete_mark (`MARK mark) + buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 491e8e823d..e32a4d9e38 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit val xml_to_string : Richpp.richpp -> string -val insert_xml : ?tags:GText.tag list -> +val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 758f383d6d..0330b8eff1 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -43,6 +43,7 @@ let message_view () : message_view = ~tag_table:Tags.Message.table () in let text_buffer = new GText.buffer buffer#as_buffer in + let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in @@ -69,7 +70,8 @@ let message_view () : message_view = new message_view_signals_impl box#as_widget push method clear = - buffer#set_text "" + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter method push level msg = let tags = match level with @@ -83,8 +85,9 @@ let message_view () : message_view = | Xml_datatype.Element (_, _, children) -> List.exists non_empty children in if non_empty (Richpp.repr msg) then begin - Ideutils.insert_xml buffer ~tags msg; - buffer#insert (*~tags*) "\n"; + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags msg; + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; push#call (level, msg) end -- cgit v1.2.3