Expose the diff printing option as an UI entry in CoqIDE.

4 files changed, 57 insertions, 19 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 63986935aa..e948360191 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -530,20 +530,31 @@ let break_coqtop coqtop workers =
 
 module PrintOpt =
 struct
-  type t = string list
+  type _ t =
+  | BoolOpt : string list -> bool t
+  | StringOpt : string list -> string t
+
+  let opt_name (type a) : a t -> string list = function
+  | BoolOpt l -> l
+  | StringOpt l -> l
+
+  let opt_data (type a) (key : a t) (v : a) = match key with
+  | BoolOpt l -> Interface.BoolValue v
+  | StringOpt l -> Interface.StringValue v
 
   (* Boolean options *)
 
-  let implicit = ["Printing"; "Implicit"]
-  let coercions = ["Printing"; "Coercions"]
-  let raw_matching = ["Printing"; "Matching"]
-  let notations = ["Printing"; "Notations"]
-  let all_basic = ["Printing"; "All"]
-  let existential = ["Printing"; "Existential"; "Instances"]
-  let universes = ["Printing"; "Universes"]
-  let unfocused = ["Printing"; "Unfocused"]
+  let implicit = BoolOpt ["Printing"; "Implicit"]
+  let coercions = BoolOpt ["Printing"; "Coercions"]
+  let raw_matching = BoolOpt ["Printing"; "Matching"]
+  let notations = BoolOpt ["Printing"; "Notations"]
+  let all_basic = BoolOpt ["Printing"; "All"]
+  let existential = BoolOpt ["Printing"; "Existential"; "Instances"]
+  let universes = BoolOpt ["Printing"; "Universes"]
+  let unfocused = BoolOpt ["Printing"; "Unfocused"]
+  let diff = StringOpt ["Diffs"]
 
-  type bool_descr = { opts : t list; init : bool; label : string }
+  type 'a descr = { opts : 'a t list; init : 'a; label : string }
 
   let bool_items = [
     { opts = [implicit]; init = false; label = "Display _implicit arguments" };
@@ -561,24 +572,32 @@ struct
     { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
   ]
 
+  let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" }
+
   (** The current status of the boolean options *)
 
   let current_state = Hashtbl.create 11
 
-  let set opt v = Hashtbl.replace current_state opt v
+  let set (type a) (opt : a t) (v : a) =
+    Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
 
   let reset () =
     let init_descr d = List.iter (fun o -> set o d.init) d.opts in
-    List.iter init_descr bool_items
+    List.iter init_descr bool_items;
+    List.iter (fun o -> set o diff_item.init) diff_item.opts
 
   let _ = reset ()
 
-  let printing_unfocused () = Hashtbl.find current_state unfocused
+  let printing_unfocused () =
+  let BoolOpt unfocused = unfocused in
+  match Hashtbl.find current_state unfocused with
+  | Interface.BoolValue b -> b
+  | _ -> assert false
 
   (** Transmitting options to coqtop *)
 
   let enforce h k =
-    let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
+    let mkopt o v acc = (o, v) :: acc in
     let opts = Hashtbl.fold mkopt current_state [] in
     eval_call (Xmlprotocol.set_options opts) h
       (function
diff --git a/ide/coq.mli b/ide/coq.mli
index 40a6dea8d3..3af0aa697e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
 
 module PrintOpt :
 sig
-  type t (** Representation of an option *)
+  type 'a t (** Representation of an option *)
 
-  type bool_descr = { opts : t list; init : bool; label : string }
+  type 'a descr = { opts : 'a t list; init : 'a; label : string }
 
-  val bool_items : bool_descr list
+  val bool_items : bool descr list
 
-  val set : t -> bool -> unit
+  val diff_item : string descr
+
+  val set : 'a t -> 'a -> unit
 
   val printing_unfocused: unit -> bool
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa816f2b8b..566532b296 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -826,6 +826,7 @@ let refresh_notebook_pos () =
 
 let menu = GAction.add_actions
 let item = GAction.add_action
+let radio = GAction.add_radio_action
 
 (** Toggle items in menus for printing options *)
 
@@ -1043,7 +1044,19 @@ let build_ui () =
       ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get));
     item "Query Pane" ~label:"_Query Pane"
       ~accel:"F1"
-      ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
+      ~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
+        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";
+      ];
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;
 
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 717c4000f5..91c529932f 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -86,6 +86,10 @@ let init () =
 \n    <menuitem action='Display universe levels' />\
 \n    <menuitem action='Display all low-level contents' />\
 \n    <menuitem action='Display unfocused goals' />\
+\n    <separator/>\
+\n    <menuitem action='Unset diff' />\
+\n    <menuitem action='Set diff' />\
+\n    <menuitem action='Set removed diff' />\
 \n  </menu>\
 \n  <menu action='Navigation'>\
 \n    <menuitem action='Forward' />\