From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 ide/ideutils.ml | 61 ++++++++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 45 insertions(+), 16 deletions(-)

(limited to 'ide/ideutils.ml')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94..03396a5a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,11 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
+(* Note: Setting the same attribute with two separate tags appears to use
+the first value applied and not the second.  I saw this trying to set the background
+color on Windows.  A clean fix, if ever needed, would be to combine the attributes
+of the tags into a single composite tag before applying.  This is left as an
+exercise for the reader. *)
 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
@@ -50,21 +55,51 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
     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
+    List.iter iter (List.rev tags)
+
+let nl_white_regex = Str.regexp "^\\( *\n *\\)"
+let diff_regex = Str.regexp "^diff."
 
 let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
   let open Xml_datatype in
+  let dtags = ref [] 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 rmark = `MARK (buf#create_mark buf#start_iter) in
+  (* insert the string, but don't apply diff highlights to white space at the begin/end of line *)
+  let rec insert_str tags s =
+    let etags = try List.hd !dtags :: tags with hd -> tags in
+    try
+      let start = Str.search_forward nl_white_regex s 0 in
+      insert_with_tags buf mark rmark etags (String.sub s 0 start);
+      insert_with_tags buf mark rmark tags (Str.matched_group 1 s);
+      let mend = Str.match_end () in
+      insert_str tags (String.sub s mend (String.length s - mend))
+    with Not_found ->
+      insert_with_tags buf mark rmark etags s
+  in
   let rec insert tags = function
-  | PCData s -> insert_with_tags buf mark rmark tags s
+  | PCData s -> insert_str tags s
   | Element (t, _, children) ->
-    let tags = try tag t :: tags with Not_found -> tags in
-    List.iter (fun xml -> insert tags xml) children
+    let (pfx, tname) = Pp.split_tag t in
+    let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in
+    let (tags, have_tag) =
+      try
+        let t = tag tname in
+        if is_diff && pfx <> Pp.end_pfx then
+          dtags := t :: !dtags;
+        if pfx = "" then
+          ((if is_diff then tags else t :: tags), true)
+        else
+          (tags, true)
+      with Not_found -> (tags, false)
+    in
+    List.iter (fun xml -> insert tags xml) children;
+    if have_tag && is_diff && pfx <> Pp.start_pfx then
+      dtags := (try List.tl !dtags with tl -> []);
   in
   let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
@@ -289,16 +324,10 @@ let coqtop_path () =
     | Some s -> s
     | None ->
       match cmd_coqtop#get with
-	| Some s -> s
-	| None ->
-	  try
-            let old_prog = Sys.executable_name in
-            let pos = String.length old_prog - 6 in
-            let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
-            in
-            let new_prog = Bytes.of_string old_prog in
-            Bytes.blit_string "coqtop" 0 new_prog i 6;
-            let new_prog = Bytes.to_string new_prog in
+      | Some s -> s
+      | None ->
+        try
+          let new_prog = System.get_toplevel_path "coqidetop" in
             if Sys.file_exists new_prog then new_prog
 	    else
 	      let in_macos_bundle =
@@ -306,8 +335,8 @@ let coqtop_path () =
 		  (Filename.dirname new_prog)
 		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
-		 else "coqtop"
-	  with Not_found -> "coqtop"
+                 else "coqidetop"
+        with Not_found -> "coqidetop"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe
-- 
cgit v1.2.3