Merge branch 'v8.6'

3 files changed, 66 insertions, 61 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 5b6bad349..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
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8ef7a0554..08f49ae5d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -500,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/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