Merge branch 'v8.6'

5 files changed, 34 insertions, 17 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 50b3f2c0a..5b6bad349 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 () -> ())
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index fe69be9e4..06a132732 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_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
+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 ~iter:(buf#get_iter_at_mark mark) text
+  else
+    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 ?(mark = `INSERT) ?(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 rmark = `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 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
-  insert tags (Richpp.repr msg)
+  let () = try insert tags (Richpp.repr msg) with _ -> () in
+  buf#delete_mark rmark
 
 let set_location = ref  (function s -> failwith "not ready")
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 491e8e823..e32a4d9e3 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/preferences.ml b/ide/preferences.ml
index 3241a962d..64327d74f 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
 
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 758f383d6..0330b8eff 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