From b253e31a22024a5bb73b6fa707e6582b4034621b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Sep 2016 16:24:37 +0200 Subject: feedback: support multiple feedback listeners So that a module can add his own and look at the traffic --- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7aec..bb8723dfe6 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -499,7 +499,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; -- cgit v1.2.3 From e8630fbd2b27a476e0570408397289a1affab86e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Sep 2016 16:25:22 +0200 Subject: xml_printer: use sensible names for putc and puts They used to be called output and output' ... --- ide/xml_printer.ml | 116 ++++++++++++++++++++++++++--------------------------- 1 file changed, 58 insertions(+), 58 deletions(-) (limited to 'ide') diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml index e7e4d0cebc..40ab4ce9cb 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 "<" + | ' ' -> puts " "; + | '>' -> puts ">" + | '<' -> puts "<" | '&' -> if p < l - 1 && text.[p + 1] = '#' then - output' '&' + putc '&' else - output "&" - | '\'' -> output "'" - | '"' -> output """ - | c -> output' c + puts "&" + | '\'' -> puts "'" + | '"' -> puts """ + | 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 "<" - | '&' -> output "&" - | c -> output' c + | '\\' -> puts "\\\\" + | '"' -> puts "\\\"" + | '<' -> puts "<" + | '&' -> puts "&" + | 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 "'; + puts "'; 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 "'; - if newl then output' '\n'; + puts "'; + 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 "'; - if newl then output' '\n'; + puts tab; + puts "'; + 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 -- cgit v1.2.3 From 6745caadf63630c1ad725402fd527ba592dbcd0e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Sep 2016 17:48:40 +0200 Subject: coqide: use Document instead of tags to detect sentences to `Skip (#4829) When one jumps from a focused area to a point after the focused zone, sentences that are already processed (in the Doc.context of the focused area) have not to be processed again (they are tagged as `Skip). Detection of such sentences was based on tags (i.e. colors) that is shaky. Now we use the sentence-marks as stored in the document data structure. --- ide/coqOps.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 5b6bad3496..741a1d6e2a 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -561,13 +561,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 -- cgit v1.2.3 From 1f4a8889f4bc4c2201080004db6371950b4ea36d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Sep 2016 15:07:09 +0200 Subject: CoqIDE: Errors are sticky (fix #4368) --- ide/coqOps.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 741a1d6e2a..52f935bf66 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; -- cgit v1.2.3