Merge PR #8260: Tweak diff options in CoqIDE

4 files changed, 23 insertions, 9 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 09a82ba91e..00d43e6e64 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1046,16 +1046,24 @@ let build_ui () =
       ~accel:"F1"
       ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane);
     GAction.group_radio_actions
-      ~callback:begin function
-        | 0 -> List.iter (fun o -> Opt.set o "off") Opt.diff_item.Opt.opts
-        | 1 -> List.iter (fun o -> Opt.set o "on") Opt.diff_item.Opt.opts
-        | 2 -> List.iter (fun o -> Opt.set o "removed") Opt.diff_item.Opt.opts
-        | _ -> assert false
+      ~init_value:(
+        let v = diffs#get in
+        List.iter (fun o -> Opt.set o v) Opt.diff_item.Opt.opts;
+        if v = "on" then 1
+        else if v = "removed" then 2
+        else 0)
+      ~callback:begin fun n ->
+        (match n with
+        | 0 -> List.iter (fun o -> Opt.set o "off"; diffs#set "off") Opt.diff_item.Opt.opts
+        | 1 -> List.iter (fun o -> Opt.set o "on"; diffs#set "on") Opt.diff_item.Opt.opts
+        | 2 -> List.iter (fun o -> Opt.set o "removed"; diffs#set "removed") Opt.diff_item.Opt.opts
+        | _ -> assert false);
+        send_to_coq (fun sn -> sn.coqops#show_goals)
         end
       [
-        radio "Unset diff" 0 ~label:"Unset _Diff";
-        radio "Set diff" 1 ~label:"Set Di_ff";
-        radio "Set removed diff" 2 ~label:"Set _Removed Diff";
+        radio "Unset diff" 0 ~label:"_Don't show diffs";
+        radio "Set diff" 1 ~label:"Show diffs: only _added";
+        radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
       ];
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 417ade51fd..d846b3abb5 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -53,10 +53,12 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
   ["Printing";"Universes"];
-  ["Printing";"Unfocused"]]
+  ["Printing";"Unfocused"];
+  ["Diffs"]]
 
 let is_known_option cmd = match Vernacprop.under_control cmd with
   | VernacSetOption (_, o, BoolValue true)
+  | VernacSetOption (_, o, StringValue _)
   | VernacUnsetOption (_, o) -> coqide_known_option o
   | _ -> false
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 526d94a939..955ee87840 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -565,6 +565,9 @@ let nanoPG =
 let user_queries =
   new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')
 
+let diffs =
+  new preference ~name:["diffs"] ~init:"off" ~repr:Repr.(string)
+
 class tag_button (box : Gtk.box Gtk.obj) =
 object (self)
 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index f3882d486d..dd2976efc2 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -102,6 +102,7 @@ val tab_length : int preference
 val highlight_current_line : bool preference
 val nanoPG : bool preference
 val user_queries : (string * string) list preference
+val diffs : string preference
 
 val save_pref : unit -> unit
 val load_pref : unit -> unit