8 files changed, 110 insertions, 90 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 50b3f2c0a..52f935bf6 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -447,7 +447,6 @@ object(self)
       | Processed, Some (id,sentence) ->
           log "Processed" id;
           remove_flag sentence `PROCESSING;
-          remove_flag sentence `ERROR;
           self#mark_as_needed sentence
       | ProcessingIn _,  Some (id,sentence) ->
           log "ProcessingIn" id;
@@ -561,13 +560,19 @@ object(self)
       condition returns true; it is fed with the number of phrases read and the
       iters enclosing the current sentence. *)
   method private fill_command_queue until queue =
+    let topstack =
+      if Doc.focused document then fst (Doc.context document) else [] in
     let rec loop n iter =
       match Sentence.find buffer iter with
       | None -> ()
       | Some (start, stop) ->
         if until n start stop then begin
           ()
-        end else if stop#backward_char#has_tag Tags.Script.processed then begin
+        end else if
+          List.exists (fun (_, s) ->
+            start#equal (buffer#get_iter_at_mark s.start) &&
+            stop#equal (buffer#get_iter_at_mark s.stop)) topstack
+        then begin
           Queue.push (`Skip (start, stop)) queue;
           loop n stop
         end else begin
@@ -785,7 +790,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/ide_slave.ml b/ide/ide_slave.ml
index 1d215f4ca..4171eb20d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -13,6 +13,10 @@ open Util
 open Pp
 open Printer
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+module CompactedDecl = Context.Compacted.Declaration
+
 (** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
     when the -ideslave option is passed to Coqtop. Currently CoqIDE is
@@ -133,7 +137,8 @@ let annotate phrase =
 (** Goal display *)
 
 let hyp_next_tac sigma env decl =
-  let (id,_,ast) = Context.Named.Declaration.to_tuple decl in
+  let id = NamedDecl.get_id decl in
+  let ast = NamedDecl.get_type decl in
   let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
   [
@@ -190,16 +195,12 @@ let process_goal sigma g =
     Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
   in
   let process_hyp d (env,l) =
-    let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
-    let d' = List.map (fun name -> let open Context.Named.Declaration in
-                                   match pi2 d with
-                                   | None -> LocalAssum (name, pi3 d)
-                                   | Some value -> LocalDef (name, value, pi3 d))
-                      (pi1 d) in
+    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in
+    let d' = CompactedDecl.to_named_context d in
       (List.fold_right Environ.push_named d' env,
-       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
   let (_env, hyps) =
-    Context.NamedList.fold process_hyp
+    Context.Compacted.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
@@ -499,7 +500,7 @@ let loop () =
   let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
   Feedback.set_logger (slave_logger xml_oc);
-  Feedback.set_feeder (slave_feeder xml_oc);
+  Feedback.add_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
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/utils/config_file.ml b/ide/utils/config_file.ml
index 4d0aabeb6..e4c613913 100644
--- a/ide/utils/config_file.ml
+++ b/ide/utils/config_file.ml
@@ -44,9 +44,6 @@
 (* ******************************************************************************** *)
 (* This code is intended to be usable without any dependencies. *)
 
-(* pipeline style, see for instance Raw.of_channel. *)
-let (|>) x f  = f x
-
 (* as List.assoc, but applies f to the element matching [key] and returns the list
 where this element has been replaced by the result of f. *)
 let rec list_assoc_remove key f = function
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
 
diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml
index e7e4d0ceb..40ab4ce9c 100644
--- a/ide/xml_printer.ml
+++ b/ide/xml_printer.ml
@@ -17,65 +17,65 @@ type t = target
 let make x = x
 
 let buffer_pcdata tmp text =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
   let l = String.length text in
   for p = 0 to l-1 do
     match text.[p] with
-      | ' ' -> output " ";
-      | '>' -> output ">"
-      | '<' -> output "&lt;"
+      | ' ' -> puts "&nbsp;";
+      | '>' -> puts "&gt;"
+      | '<' -> puts "&lt;"
       | '&' ->
         if p < l - 1 && text.[p + 1] = '#' then
-          output' '&'
+          putc '&'
         else
-          output "&amp;"
-      | '\'' -> output "&apos;"
-      | '"' -> output "&quot;"
-      | c -> output' c
+          puts "&amp;"
+      | '\'' -> puts "&apos;"
+      | '"' -> puts "&quot;"
+      | c -> putc c
   done
 
 let buffer_attr tmp (n,v) =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  output' ' ';
-  output n;
-  output "=\"";
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
+  putc ' ';
+  puts n;
+  puts "=\"";
   let l = String.length v in
   for p = 0 to l - 1 do
     match v.[p] with
-      | '\\' -> output "\\\\"
-      | '"' -> output "\\\""
-      | '<' -> output "&lt;"
-      | '&' -> output "&amp;"
-      | c -> output' c
+      | '\\' -> puts "\\\\"
+      | '"' -> puts "\\\""
+      | '<' -> puts "&lt;"
+      | '&' -> puts "&amp;"
+      | c -> putc c
   done;
-  output' '"'
+  putc '"'
 
 let to_buffer tmp x =
   let pcdata = ref false in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
   let rec loop = function
     | Element (tag,alist,[]) ->
-      output' '<';
-      output tag;
+      putc '<';
+      puts tag;
       List.iter (buffer_attr tmp) alist;
-      output "/>";
+      puts "/>";
       pcdata := false;
     | Element (tag,alist,l) ->
-      output' '<';
-      output tag;
+      putc '<';
+      puts tag;
       List.iter (buffer_attr tmp) alist;
-      output' '>';
+      putc '>';
       pcdata := false;
       List.iter loop l;
-      output "</";
-      output tag;
-      output' '>';
+      puts "</";
+      puts tag;
+      putc '>';
       pcdata := false;
     | PCData text ->
-      if !pcdata then output' ' ';
+      if !pcdata then putc ' ';
       buffer_pcdata tmp text;
       pcdata := true;
   in
@@ -93,42 +93,42 @@ let to_string x =
 
 let to_string_fmt x =
   let tmp = Buffer.create 200 in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
   let rec loop ?(newl=false) tab = function
     | Element (tag, alist, []) ->
-      output tab;
-      output' '<';
-      output tag;
+      puts tab;
+      putc '<';
+      puts tag;
       List.iter (buffer_attr tmp) alist;
-      output "/>";
-      if newl then output' '\n';
+      puts "/>";
+      if newl then putc '\n';
     | Element (tag, alist, [PCData text]) ->
-      output tab;
-      output' '<';
-      output tag;
+      puts tab;
+      putc '<';
+      puts tag;
       List.iter (buffer_attr tmp) alist;
-      output ">";
+      puts ">";
       buffer_pcdata tmp text;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
+      puts "</";
+      puts tag;
+      putc '>';
+      if newl then putc '\n';
     | Element (tag, alist, l) ->
-      output tab;
-      output' '<';
-      output tag;
+      puts tab;
+      putc '<';
+      puts tag;
       List.iter (buffer_attr tmp) alist;
-      output ">\n";
+      puts ">\n";
       List.iter (loop ~newl:true (tab^"  ")) l;
-      output tab;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
+      puts tab;
+      puts "</";
+      puts tag;
+      putc '>';
+      if newl then putc '\n';
     | PCData text ->
       buffer_pcdata tmp text;
-      if newl then output' '\n';
+      if newl then putc '\n';
   in
   loop "" x;
   Buffer.contents tmp