diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 47 | ||||
| -rw-r--r-- | ide/coq.mli | 10 | ||||
| -rw-r--r-- | ide/coqide.ml | 21 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 4 | ||||
| -rw-r--r-- | ide/idetop.ml | 23 | ||||
| -rw-r--r-- | ide/ideutils.ml | 43 | ||||
| -rw-r--r-- | ide/preferences.ml | 25 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 |
8 files changed, 143 insertions, 31 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..09a82ba91e 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; @@ -1106,15 +1119,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 0c3328ee08..854b1abe31 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 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 = |