aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml47
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coq_lex.mll6
-rw-r--r--ide/coqide.ml29
-rw-r--r--ide/coqide_ui.ml4
-rw-r--r--ide/idetop.ml11
-rw-r--r--ide/preferences.ml3
-rw-r--r--ide/preferences.mli1
8 files changed, 81 insertions, 30 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/coq_lex.mll b/ide/coq_lex.mll
index 1fdd7317b5..b6654f6d7a 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+
let string = "\"" _+ "\""
-let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
+let alpha = ['a'-'z' 'A'-'Z']
+
+let ident = alpha (alpha | number | '_' | "'")*
+
+let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number
diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa816f2b8b..00d43e6e64 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,27 @@ 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
+ ~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:"_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;
@@ -1106,15 +1127,15 @@ let build_ui () =
];
alpha_items templates_menu "Template" Coq_commands.commands;
- let qitem s sc ?(dots = true) =
- let query = if dots then s ^ "..." else s in
+ let qitem s sc =
+ let query = s ^ "..." in
item s ~label:("_"^s)
~accel:(modifier_for_queries#get^sc)
~callback:(Query.query query)
in
menu queries_menu [
item "Queries" ~label:"_Queries";
- qitem "Search" "K" ~dots:false;
+ qitem "Search" "K";
qitem "Check" "C";
qitem "Print" "P";
qitem "About" "A";
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' />\
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 965bb913ff..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
@@ -211,15 +213,13 @@ let add_diffs oldp newp intf =
{ 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 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
+ let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
try
Some (add_diffs oldp (Some newp) intf)
with Pp_diff.Diff_Failure _ -> Some intf
@@ -530,9 +530,6 @@ 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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 00:44:46 +0000