Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)

4 files changed, 86 insertions, 9 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 0c3328ee08..965bb913ff 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -202,13 +202,30 @@ let export_pre_goals pgs =
     Interface.given_up_goals = pgs.Proof.given_up_goals
   }
 
+let add_diffs oldp newp intf =
+  let open Interface in
+  let (hyps_pp_list, concl_pp) = Proof_diffs.diff_first_goal oldp newp in
+  match intf.fg_goals with
+  | [] -> intf
+  | first_goal :: tl ->
+    { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl }
+
 let goals () =
+  let oldp =
+    try Some (Proof_global.give_me_the_proof ())
+    with Proof_global.NoCurrentProof -> None in
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let pfts = Proof_global.give_me_the_proof () in
-    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
-  with Proof_global.NoCurrentProof -> None
+    let newp = Proof_global.give_me_the_proof () in
+    let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in
+    if Proof_diffs.show_diffs () then
+      try
+        Some (add_diffs oldp (Some newp) intf)
+      with Pp_diff.Diff_Failure _ -> Some intf
+    else
+      Some intf
+  with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
   try
@@ -513,6 +530,9 @@ let () = Usage.add_to_usage "coqidetop"
 let islave_init ~opts extra_args =
   let args = parse extra_args in
   CoqworkmgrApi.(init High);
+  let open Coqargs in
+    if not opts.diffs_set then
+      Proof_diffs.write_diffs_option "on";
   opts, args
 
 let () =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e96b992999..960beb8455 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 =
+    try
+      let _ = Str.search_forward nl_white_regex s 0 in
+      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 -> begin
+      let etags = try List.hd !dtags :: tags with hd -> tags in
+      insert_with_tags buf mark rmark etags s
+      end
+  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
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11aaf6e8cc..526d94a939 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -25,6 +25,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 (** Generic preferences *)
@@ -215,15 +216,17 @@ object
     string_of_bool tag.tag_bold;
     string_of_bool tag.tag_italic;
     string_of_bool tag.tag_underline;
+    string_of_bool tag.tag_strikethrough;
   ]
   method into = function
-  | [fg; bg; bd; it; ul] ->
+  | [fg; bg; bd; it; ul; st] ->
     (try Some {
       tag_fg_color = _to fg;
       tag_bg_color = _to bg;
       tag_bold = bool_of_string bd;
       tag_italic = bool_of_string it;
       tag_underline = bool_of_string ul;
+      tag_strikethrough = bool_of_string st;
       }
     with _ -> None)
   | _ -> None
@@ -429,12 +432,13 @@ let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
 
-let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) ?(strikethrough = false) () = {
   tag_fg_color = fg;
   tag_bg_color = bg;
   tag_bold = bold;
   tag_italic = italic;
   tag_underline = underline;
+  tag_strikethrough = strikethrough;
 }
 
 let create_tag name default =
@@ -470,6 +474,12 @@ let create_tag name default =
       tag#set_property (`UNDERLINE_SET true);
       tag#set_property (`UNDERLINE `SINGLE)
     end;
+    begin match pref#get.tag_strikethrough with
+    | false -> tag#set_property (`STRIKETHROUGH_SET false)
+    | true ->
+      tag#set_property (`STRIKETHROUGH_SET true);
+      tag#set_property (`STRIKETHROUGH true)
+    end;
   in
   let iter table =
     let tag = GText.tag ~name () in
@@ -480,6 +490,8 @@ let create_tag name default =
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
   tags := Util.String.Map.add name pref !tags
 
+(* note these appear to only set the defaults; they don't override
+the user selection from the Edit/Preferences/Tags dialog *)
 let () =
   let iter (name, tag) = create_tag name tag in
   List.iter iter [
@@ -498,6 +510,10 @@ let () =
     ("tactic.keyword", make_tag ());
     ("tactic.primitive", make_tag ());
     ("tactic.string", make_tag ());
+    ("diff.added", make_tag ~bg:"#b6f1c0" ~underline:true ());
+    ("diff.removed", make_tag ~bg:"#f6b9c1" ~strikethrough:true ());
+    ("diff.added.bg", make_tag ~bg:"#e9feee" ());
+    ("diff.removed.bg", make_tag ~bg:"#fce9eb" ());
   ]
 
 let processed_color =
@@ -561,6 +577,7 @@ object (self)
   val bold = GButton.toggle_button ()
   val italic = GButton.toggle_button ()
   val underline = GButton.toggle_button ()
+  val strikethrough = GButton.toggle_button ()
 
   method set_tag tag =
     let track c but set = match c with
@@ -574,6 +591,7 @@ object (self)
     bold#set_active tag.tag_bold;
     italic#set_active tag.tag_italic;
     underline#set_active tag.tag_underline;
+    strikethrough#set_active tag.tag_strikethrough;
 
   method tag =
     let get but set =
@@ -586,6 +604,7 @@ object (self)
       tag_bold = bold#active;
       tag_italic = italic#active;
       tag_underline = underline#active;
+      tag_strikethrough = strikethrough#active;
     }
 
   initializer
@@ -599,6 +618,7 @@ object (self)
     set_stock bold `BOLD;
     set_stock italic `ITALIC;
     set_stock underline `UNDERLINE;
+    set_stock strikethrough `STRIKETHROUGH;
     box#pack fg_color#coerce;
     box#pack fg_unset#coerce;
     box#pack bg_color#coerce;
@@ -606,6 +626,7 @@ object (self)
     box#pack bold#coerce;
     box#pack italic#coerce;
     box#pack underline#coerce;
+    box#pack strikethrough#coerce;
     let cb but obj = obj#set_sensitive (not but#active) in
     let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
     let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028aee4..f3882d486d 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -21,6 +21,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 class type ['a] repr =