From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- ide/preferences.ml | 1274 +++++++++++++++++++++++++++++----------------------- 1 file changed, 714 insertions(+), 560 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index f7cc27a5..f0fd45d7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -17,19 +17,67 @@ let style_manager = GSourceView2.source_style_scheme_manager ~default:true let () = style_manager#set_search_path ((Minilib.coqide_data_dirs ())@style_manager#search_path) -let get_config_file name = - let find_config dir = Sys.file_exists (Filename.concat dir name) in - let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in - Filename.concat config_dir name +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} -(* Small hack to handle v8.3 to v8.4 change in configuration file *) -let loaded_pref_file = - try get_config_file "coqiderc" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc" +(** Generic preferences *) -let loaded_accel_file = - try get_config_file "coqide.keys" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" +type obj = { + set : string list -> unit; + get : unit -> string list; +} + +let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty +let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty + +class type ['a] repr = +object + method into : string list -> 'a option + method from : 'a -> string list +end + +class ['a] preference_signals ~(changed : 'a GUtil.signal) = +object + inherit GUtil.ml_signals [changed#disconnect] + method changed = changed#connect ~after +end + +class ['a] preference ~(name : string list) ~(init : 'a) ~(repr : 'a repr) = +object (self) + initializer + let set v = match repr#into v with None -> () | Some s -> self#set s in + let get () = repr#from self#get in + let obj = { set = set; get = get; } in + let name = String.concat "." name in + if Util.String.Map.mem name !preferences then + invalid_arg ("Preference " ^ name ^ " already exists") + else + preferences := Util.String.Map.add name obj !preferences + + val default = init + val mutable data = init + val changed : 'a GUtil.signal = new GUtil.signal () + val name : string list = name + method connect = new preference_signals ~changed + method get = data + method set (n : 'a) = data <- n; changed#call n + method reset () = self#set default + method default = default +end + +let stick (pref : 'a preference) (obj : #GObj.widget as 'obj) + (cb : 'a -> unit) = + let _ = cb pref#get in + let p_id = pref#connect#changed (fun v -> cb v) in + let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in + () + +(** Useful marshallers *) let mod_to_str m = match m with @@ -74,359 +122,537 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] + +let line_end_of_string = function +| "unix" -> `UNIX +| "windows" -> `WINDOWS +| _ -> `DEFAULT + +let line_end_to_string = function +| `UNIX -> "unix" +| `WINDOWS -> "windows" +| `DEFAULT -> "default" + +let use_default_doc_url = "(automatic)" + +module Repr = +struct + +let string : string repr = +object + method from s = [s] + method into = function [s] -> Some s | _ -> None +end + +let string_pair : (string * string) repr = +object + method from (s1, s2) = [s1; s2] + method into = function [s1; s2] -> Some (s1, s2) | _ -> None +end + +let string_list : string list repr = +object + method from s = s + method into s = Some s +end + +let string_pair_list (sep : char) : (string * string) list repr = +object + val sep' = String.make 1 sep + method from = CList.map (fun (s1, s2) -> CString.concat sep' [s1; s2]) + method into l = + try + Some (CList.map (fun s -> + let split = CString.split sep s in + CList.nth split 0, CList.nth split 1) l) + with Failure _ -> None +end + +let bool : bool repr = +object + method from s = [string_of_bool s] + method into = function + | ["true"] -> Some true + | ["false"] -> Some false + | _ -> None +end + +let int : int repr = +object + method from s = [string_of_int s] + method into = function + | [i] -> (try Some (int_of_string i) with _ -> None) + | _ -> None +end + +let option (r : 'a repr) : 'a option repr = +object + method from = function None -> [] | Some v -> "" :: r#from v + method into = function + | [] -> Some None + | "" :: s -> Some (r#into s) + | _ -> None +end + +let custom (from : 'a -> string) (into : string -> 'a) : 'a repr = +object + method from x = try [from x] with _ -> [] + method into = function + | [s] -> (try Some (into s) with _ -> None) + | _ -> None +end + +let tag : tag repr = +let _to s = if s = "" then None else Some s in +let _of = function None -> "" | Some s -> s in +object + method from tag = [ + _of tag.tag_fg_color; + _of tag.tag_bg_color; + string_of_bool tag.tag_bold; + string_of_bool tag.tag_italic; + string_of_bool tag.tag_underline; + ] + method into = function + | [fg; bg; bd; it; ul] -> + (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; + } + with _ -> None) + | _ -> None +end + +end + +let get_config_file name = + let find_config dir = Sys.file_exists (Filename.concat dir name) in + let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in + Filename.concat config_dir name + +(* Small hack to handle v8.3 to v8.4 change in configuration file *) +let loaded_pref_file = + try get_config_file "coqiderc" + with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc" + +let loaded_accel_file = + try get_config_file "coqide.keys" + with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" (** Hooks *) -let refresh_style_hook = ref (fun () -> ()) -let refresh_language_hook = ref (fun () -> ()) -let refresh_editor_hook = ref (fun () -> ()) -let refresh_toolbar_hook = ref (fun () -> ()) -let contextual_menus_on_goal_hook = ref (fun x -> ()) -let resize_window_hook = ref (fun () -> ()) -let refresh_tabs_hook = ref (fun () -> ()) +(** New style preferences *) -type pref = - { - mutable cmd_coqtop : string option; - mutable cmd_coqc : string; - mutable cmd_make : string; - mutable cmd_coqmakefile : string; - mutable cmd_coqdoc : string; +let cmd_coqtop = + new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) - mutable source_language : string; - mutable source_style : string; +let cmd_coqc = + new preference ~name:["cmd_coqc"] ~init:"coqc" ~repr:Repr.(string) - mutable global_auto_revert : bool; - mutable global_auto_revert_delay : int; +let cmd_make = + new preference ~name:["cmd_make"] ~init:"make" ~repr:Repr.(string) - mutable auto_save : bool; - mutable auto_save_delay : int; - mutable auto_save_name : string * string; +let cmd_coqmakefile = + new preference ~name:["cmd_coqmakefile"] ~init:"coq_makefile -o makefile *.v" ~repr:Repr.(string) - mutable read_project : project_behavior; - mutable project_file_name : string; - mutable project_path : string option; +let cmd_coqdoc = + new preference ~name:["cmd_coqdoc"] ~init:"coqdoc -q -g" ~repr:Repr.(string) - mutable encoding : inputenc; +let source_language = + new preference ~name:["source_language"] ~init:"coq" ~repr:Repr.(string) - mutable automatic_tactics : string list; - mutable cmd_print : string; +let source_style = + new preference ~name:["source_style"] ~init:"coq_style" ~repr:Repr.(string) - mutable modifier_for_navigation : string; - mutable modifier_for_templates : string; - mutable modifier_for_tactics : string; - mutable modifier_for_display : string; - mutable modifiers_valid : string; +let global_auto_revert = + new preference ~name:["global_auto_revert"] ~init:false ~repr:Repr.(bool) - mutable cmd_browse : string; - mutable cmd_editor : string; +let global_auto_revert_delay = + new preference ~name:["global_auto_revert_delay"] ~init:10000 ~repr:Repr.(int) - mutable text_font : Pango.font_description; +let auto_save = + new preference ~name:["auto_save"] ~init:true ~repr:Repr.(bool) - mutable doc_url : string; - mutable library_url : string; +let auto_save_delay = + new preference ~name:["auto_save_delay"] ~init:10000 ~repr:Repr.(int) - mutable show_toolbar : bool; - mutable contextual_menus_on_goal : bool; - mutable window_width : int; - mutable window_height :int; - mutable query_window_width : int; - mutable query_window_height : int; -(* - mutable use_utf8_notation : bool; -*) - mutable auto_complete : bool; - mutable stop_before : bool; - mutable reset_on_tab_switch : bool; - mutable vertical_tabs : bool; - mutable opposite_tabs : bool; - - mutable background_color : string; - mutable processing_color : string; - mutable processed_color : string; - mutable error_color : string; - mutable error_fg_color : string; - - mutable dynamic_word_wrap : bool; - mutable show_line_number : bool; - mutable auto_indent : bool; - mutable show_spaces : bool; - mutable show_right_margin : bool; - mutable show_progress_bar : bool; - mutable spaces_instead_of_tabs : bool; - mutable tab_length : int; - mutable highlight_current_line : bool; - - mutable nanoPG : bool; +let auto_save_name = + new preference ~name:["auto_save_name"] ~init:("#","#") ~repr:Repr.(string_pair) + +let read_project = + let repr = Repr.custom string_of_project_behavior project_behavior_of_string in + new preference ~name:["read_project"] ~init:Append_args ~repr + +let project_file_name = + new preference ~name:["project_file_name"] ~init:"_CoqProject" ~repr:Repr.(string) + +let project_path = + new preference ~name:["project_path"] ~init:None ~repr:Repr.(option string) + +let encoding = + let repr = Repr.custom string_of_inputenc inputenc_of_string in + let init = if Sys.os_type = "Win32" then Eutf8 else Elocale in + new preference ~name:["encoding"] ~init ~repr + +let automatic_tactics = + let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in + new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list) +let cmd_print = + new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string) + +let attach_modifiers (pref : string preference) prefix = + let cb mds = + let mds = str_to_mod_list mds in + let change ~path ~key ~modi ~changed = + if CString.is_sub prefix path 0 then + ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path) + in + GtkData.AccelMap.foreach change + in + pref#connect#changed cb + +let modifier_for_navigation = + new preference ~name:["modifier_for_navigation"] ~init:"" ~repr:Repr.(string) + +let modifier_for_templates = + new preference ~name:["modifier_for_templates"] ~init:"" ~repr:Repr.(string) + +let modifier_for_tactics = + new preference ~name:["modifier_for_tactics"] ~init:"" ~repr:Repr.(string) + +let modifier_for_display = + new preference ~name:["modifier_for_display"] ~init:"" ~repr:Repr.(string) + +let modifier_for_queries = + new preference ~name:["modifier_for_queries"] ~init:"" ~repr:Repr.(string) + +let _ = attach_modifiers modifier_for_navigation "/Navigation/" +let _ = attach_modifiers modifier_for_templates "/Templates/" +let _ = attach_modifiers modifier_for_tactics "/Tactics/" +let _ = attach_modifiers modifier_for_display "/View/" +let _ = attach_modifiers modifier_for_queries "/Queries/" + +let modifiers_valid = + new preference ~name:["modifiers_valid"] ~init:"" ~repr:Repr.(string) + +let cmd_browse = + new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string) + +let cmd_editor = + let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in + new preference ~name:["cmd_editor"] ~init ~repr:Repr.(string) + +let text_font = + let init = match Coq_config.gtk_platform with + | `QUARTZ -> "Arial Unicode MS 11" + | _ -> "Monospace 10" + in + new preference ~name:["text_font"] ~init ~repr:Repr.(string) + +let doc_url = +object + inherit [string] preference + ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) + as super + + method set v = + if not (Flags.is_standard_doc_url v) && + v <> use_default_doc_url && + (* Extra hack to support links to last released doc version *) + v <> Coq_config.wwwcoq ^ "doc" && + v <> Coq_config.wwwcoq ^ "doc/" + then super#set v + +end + +let library_url = + new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string) + +let show_toolbar = + new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool) + +let contextual_menus_on_goal = + new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool) + +let window_width = + new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int) + +let window_height = + new preference ~name:["window_height"] ~init:600 ~repr:Repr.(int) + +let auto_complete = + new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) + +let stop_before = + new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) + +let reset_on_tab_switch = + new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) + +let line_ending = + let repr = Repr.custom line_end_to_string line_end_of_string in + new preference ~name:["line_ending"] ~init:`DEFAULT ~repr + +let vertical_tabs = + new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) + +let opposite_tabs = + new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool) + +let background_color = + new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) + +let attach_bg (pref : string preference) (tag : GText.tag) = + pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c)) + +let attach_fg (pref : string preference) (tag : GText.tag) = + pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c)) + +let processing_color = + new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) + +let _ = attach_bg processing_color Tags.Script.to_process +let _ = attach_bg processing_color Tags.Script.incomplete + +let tags = ref Util.String.Map.empty + +let list_tags () = !tags + +let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = { + tag_fg_color = fg; + tag_bg_color = bg; + tag_bold = bold; + tag_italic = italic; + tag_underline = underline; } -let use_default_doc_url = "(automatic)" +let create_tag name default = + let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in + let set_tag tag = + begin match pref#get.tag_bg_color with + | None -> tag#set_property (`BACKGROUND_SET false) + | Some c -> + tag#set_property (`BACKGROUND_SET true); + tag#set_property (`BACKGROUND c) + end; + begin match pref#get.tag_fg_color with + | None -> tag#set_property (`FOREGROUND_SET false) + | Some c -> + tag#set_property (`FOREGROUND_SET true); + tag#set_property (`FOREGROUND c) + end; + begin match pref#get.tag_bold with + | false -> tag#set_property (`WEIGHT_SET false) + | true -> + tag#set_property (`WEIGHT_SET true); + tag#set_property (`WEIGHT `BOLD) + end; + begin match pref#get.tag_italic with + | false -> tag#set_property (`STYLE_SET false) + | true -> + tag#set_property (`STYLE_SET true); + tag#set_property (`STYLE `ITALIC) + end; + begin match pref#get.tag_underline with + | false -> tag#set_property (`UNDERLINE_SET false) + | true -> + tag#set_property (`UNDERLINE_SET true); + tag#set_property (`UNDERLINE `SINGLE) + end; + in + let iter table = + let tag = GText.tag ~name () in + table#add tag#as_tag; + ignore (pref#connect#changed (fun _ -> set_tag tag)); + set_tag tag; + in + List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; + tags := Util.String.Map.add name pref !tags -let current = { - cmd_coqtop = None; - cmd_coqc = "coqc"; - cmd_make = "make"; - cmd_coqmakefile = "coq_makefile -o makefile *.v"; - cmd_coqdoc = "coqdoc -q -g"; - cmd_print = "lpr"; +let () = + let iter (name, tag) = create_tag name tag in + List.iter iter [ + ("constr.evar", make_tag ()); + ("constr.keyword", make_tag ~fg:"dark green" ()); + ("constr.notation", make_tag ()); + ("constr.path", make_tag ()); + ("constr.reference", make_tag ~fg:"navy"()); + ("constr.type", make_tag ~fg:"#008080" ()); + ("constr.variable", make_tag ()); + ("message.debug", make_tag ()); + ("message.error", make_tag ()); + ("message.warning", make_tag ()); + ("module.definition", make_tag ~fg:"orange red" ~bold:true ()); + ("module.keyword", make_tag ()); + ("tactic.keyword", make_tag ()); + ("tactic.primitive", make_tag ()); + ("tactic.string", make_tag ()); + ] - global_auto_revert = false; - global_auto_revert_delay = 10000; +let processed_color = + new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string) - auto_save = true; - auto_save_delay = 10000; - auto_save_name = "#","#"; +let _ = attach_bg processed_color Tags.Script.processed +let _ = attach_bg processed_color Tags.Proof.highlight - source_language = "coq"; - source_style = "coq_style"; +let error_color = + new preference ~name:["error_color"] ~init:"#FFCCCC" ~repr:Repr.(string) - read_project = Append_args; - project_file_name = "_CoqProject"; - project_path = None; +let _ = attach_bg error_color Tags.Script.error_bg - encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; +let error_fg_color = + new preference ~name:["error_fg_color"] ~init:"red" ~repr:Repr.(string) - automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; - "auto with *"; "intuition" ]; +let _ = attach_fg error_fg_color Tags.Script.error - modifier_for_navigation = ""; - modifier_for_templates = ""; - modifier_for_tactics = ""; - modifier_for_display = ""; - modifiers_valid = ""; +let dynamic_word_wrap = + new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool) +let show_line_number = + new preference ~name:["show_line_number"] ~init:false ~repr:Repr.(bool) - cmd_browse = Flags.browser_cmd_fmt; - cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s"; +let auto_indent = + new preference ~name:["auto_indent"] ~init:false ~repr:Repr.(bool) -(* text_font = Pango.Font.from_string "sans 12";*) - text_font = Pango.Font.from_string (match Coq_config.gtk_platform with - |`QUARTZ -> "Arial Unicode MS 11" - |_ -> "Monospace 10"); +let show_spaces = + new preference ~name:["show_spaces"] ~init:true ~repr:Repr.(bool) - doc_url = Coq_config.wwwrefman; - library_url = Coq_config.wwwstdlib; +let show_right_margin = + new preference ~name:["show_right_margin"] ~init:false ~repr:Repr.(bool) - show_toolbar = true; - contextual_menus_on_goal = true; - window_width = 800; - window_height = 600; - query_window_width = 600; - query_window_height = 400; -(* - use_utf8_notation = false; -*) - auto_complete = false; - stop_before = true; - reset_on_tab_switch = false; - vertical_tabs = false; - opposite_tabs = false; - - background_color = Tags.default_color; - processed_color = Tags.default_processed_color; - processing_color = Tags.default_processing_color; - error_color = Tags.default_error_color; - error_fg_color = Tags.default_error_fg_color; - - dynamic_word_wrap = false; - show_line_number = false; - auto_indent = false; - show_spaces = true; - show_right_margin = false; - show_progress_bar = true; - spaces_instead_of_tabs = true; - tab_length = 2; - highlight_current_line = false; - - nanoPG = false; - } +let show_progress_bar = + new preference ~name:["show_progress_bar"] ~init:true ~repr:Repr.(bool) + +let spaces_instead_of_tabs = + new preference ~name:["spaces_instead_of_tabs"] ~init:true ~repr:Repr.(bool) + +let tab_length = + new preference ~name:["tab_length"] ~init:2 ~repr:Repr.(int) + +let highlight_current_line = + new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool) + +let nanoPG = + new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) + +let user_queries = + new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$') + +class tag_button (box : Gtk.box Gtk.obj) = +object (self) + + inherit GObj.widget box + + val fg_color = GButton.color_button () + val fg_unset = GButton.toggle_button () + val bg_color = GButton.color_button () + val bg_unset = GButton.toggle_button () + val bold = GButton.toggle_button () + val italic = GButton.toggle_button () + val underline = GButton.toggle_button () + + method set_tag tag = + let track c but set = match c with + | None -> set#set_active true + | Some c -> + set#set_active false; + but#set_color (Tags.color_of_string c) + in + track tag.tag_bg_color bg_color bg_unset; + track tag.tag_fg_color fg_color fg_unset; + bold#set_active tag.tag_bold; + italic#set_active tag.tag_italic; + underline#set_active tag.tag_underline; + + method tag = + let get but set = + if set#active then None + else Some (Tags.string_of_color but#color) + in + { + tag_bg_color = get bg_color bg_unset; + tag_fg_color = get fg_color fg_unset; + tag_bold = bold#active; + tag_italic = italic#active; + tag_underline = underline#active; + } + + initializer + let box = new GPack.box box in + let set_stock button stock = + let stock = GMisc.image ~stock ~icon_size:`BUTTON () in + button#set_image stock#coerce + in + set_stock fg_unset `CANCEL; + set_stock bg_unset `CANCEL; + set_stock bold `BOLD; + set_stock italic `ITALIC; + set_stock underline `UNDERLINE; + box#pack fg_color#coerce; + box#pack fg_unset#coerce; + box#pack bg_color#coerce; + box#pack bg_unset#coerce; + box#pack bold#coerce; + box#pack italic#coerce; + box#pack underline#coerce; + let cb but obj = obj#set_sensitive (not but#active) in + let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in + let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in + () + +end + +let tag_button () = + let box = GPack.hbox () in + new tag_button (Gobject.unsafe_cast box#as_widget) + +(** Old style preferences *) let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in - let p = current in - - let add = Util.String.Map.add in - let (++) x f = f x in - Util.String.Map.empty ++ - add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ - add "cmd_coqc" [p.cmd_coqc] ++ - add "cmd_make" [p.cmd_make] ++ - add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ - add "cmd_coqdoc" [p.cmd_coqdoc] ++ - add "source_language" [p.source_language] ++ - add "source_style" [p.source_style] ++ - add "global_auto_revert" [string_of_bool p.global_auto_revert] ++ - add "global_auto_revert_delay" - [string_of_int p.global_auto_revert_delay] ++ - add "auto_save" [string_of_bool p.auto_save] ++ - add "auto_save_delay" [string_of_int p.auto_save_delay] ++ - add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++ - - add "project_options" [string_of_project_behavior p.read_project] ++ - add "project_file_name" [p.project_file_name] ++ - add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++ - - add "encoding" [string_of_inputenc p.encoding] ++ - - add "automatic_tactics" p.automatic_tactics ++ - add "cmd_print" [p.cmd_print] ++ - add "modifier_for_navigation" [p.modifier_for_navigation] ++ - add "modifier_for_templates" [p.modifier_for_templates] ++ - add "modifier_for_tactics" [p.modifier_for_tactics] ++ - add "modifier_for_display" [p.modifier_for_display] ++ - add "modifiers_valid" [p.modifiers_valid] ++ - add "cmd_browse" [p.cmd_browse] ++ - add "cmd_editor" [p.cmd_editor] ++ - - add "text_font" [Pango.Font.to_string p.text_font] ++ - - add "doc_url" [p.doc_url] ++ - add "library_url" [p.library_url] ++ - add "show_toolbar" [string_of_bool p.show_toolbar] ++ - add "contextual_menus_on_goal" - [string_of_bool p.contextual_menus_on_goal] ++ - add "window_height" [string_of_int p.window_height] ++ - add "window_width" [string_of_int p.window_width] ++ - add "query_window_height" [string_of_int p.query_window_height] ++ - add "query_window_width" [string_of_int p.query_window_width] ++ - add "auto_complete" [string_of_bool p.auto_complete] ++ - add "stop_before" [string_of_bool p.stop_before] ++ - add "reset_on_tab_switch" [string_of_bool p.reset_on_tab_switch] ++ - add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ - add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ - add "background_color" [p.background_color] ++ - add "processing_color" [p.processing_color] ++ - add "processed_color" [p.processed_color] ++ - add "error_color" [p.error_color] ++ - add "error_fg_color" [p.error_fg_color] ++ - add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++ - add "show_line_number" [string_of_bool p.show_line_number] ++ - add "auto_indent" [string_of_bool p.auto_indent] ++ - add "show_spaces" [string_of_bool p.show_spaces] ++ - add "show_right_margin" [string_of_bool p.show_right_margin] ++ - add "show_progress_bar" [string_of_bool p.show_progress_bar] ++ - add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++ - add "tab_length" [string_of_int p.tab_length] ++ - add "highlight_current_line" [string_of_bool p.highlight_current_line] ++ - add "nanoPG" [string_of_bool p.nanoPG] ++ - Config_lexer.print_file pref_file + let add = Util.String.Map.add in + let fold key obj accu = add key (obj.get ()) accu in + let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in + let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in + Config_lexer.print_file pref_file prefs let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in - let np = current in - let set k f = try let v = Util.String.Map.find k m in f v with _ -> () in - let set_hd k f = set k (fun v -> f (List.hd v)) in - let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in - let set_int k f = set_hd k (fun v -> f (int_of_string v)) in - let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in - let set_command_with_pair_compat k f = - set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) + let iter name v = + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences in - let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ -> Some h)) in - set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v); - set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); - set_hd "cmd_make" (fun v -> np.cmd_make <- v); - set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); - set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v); - set_hd "source_language" (fun v -> np.source_language <- v); - set_hd "source_style" (fun v -> np.source_style <- v); - set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v); - set_int "global_auto_revert_delay" - (fun v -> np.global_auto_revert_delay <- v); - set_bool "auto_save" (fun v -> np.auto_save <- v); - set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v); - set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2)); - set_hd "encoding" (fun v -> np.encoding <- (inputenc_of_string v)); - set_hd "project_options" - (fun v -> np.read_project <- (project_behavior_of_string v)); - set_hd "project_file_name" (fun v -> np.project_file_name <- v); - set_option "project_path" (fun v -> np.project_path <- v); - set "automatic_tactics" - (fun v -> np.automatic_tactics <- v); - set_hd "cmd_print" (fun v -> np.cmd_print <- v); - set_hd "modifier_for_navigation" - (fun v -> np.modifier_for_navigation <- v); - set_hd "modifier_for_templates" - (fun v -> np.modifier_for_templates <- v); - set_hd "modifier_for_tactics" - (fun v -> np.modifier_for_tactics <- v); - set_hd "modifier_for_display" - (fun v -> np.modifier_for_display <- v); - set_hd "modifiers_valid" - (fun v -> - np.modifiers_valid <- v); - set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v); - set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v); - set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v); - set_hd "doc_url" (fun v -> - if not (Flags.is_standard_doc_url v) && - v <> use_default_doc_url && - (* Extra hack to support links to last released doc version *) - v <> Coq_config.wwwcoq ^ "doc" && - v <> Coq_config.wwwcoq ^ "doc/" - then - (* ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*) - np.doc_url <- v); - set_hd "library_url" (fun v -> np.library_url <- v); - set_bool "show_toolbar" (fun v -> np.show_toolbar <- v); - set_bool "contextual_menus_on_goal" - (fun v -> np.contextual_menus_on_goal <- v); - set_int "window_width" (fun v -> np.window_width <- v); - set_int "window_height" (fun v -> np.window_height <- v); - set_int "query_window_width" (fun v -> np.query_window_width <- v); - set_int "query_window_height" (fun v -> np.query_window_height <- v); - set_bool "auto_complete" (fun v -> np.auto_complete <- v); - set_bool "stop_before" (fun v -> np.stop_before <- v); - set_bool "reset_on_tab_switch" (fun v -> np.reset_on_tab_switch <- v); - set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); - set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); - set_hd "background_color" (fun v -> np.background_color <- v); - set_hd "processing_color" (fun v -> np.processing_color <- v); - set_hd "processed_color" (fun v -> np.processed_color <- v); - set_hd "error_color" (fun v -> np.error_color <- v); - set_hd "error_fg_color" (fun v -> np.error_fg_color <- v); - set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v); - set_bool "show_line_number" (fun v -> np.show_line_number <- v); - set_bool "auto_indent" (fun v -> np.auto_indent <- v); - set_bool "show_spaces" (fun v -> np.show_spaces <- v); - set_bool "show_right_margin" (fun v -> np.show_right_margin <- v); - set_bool "show_progress_bar" (fun v -> np.show_progress_bar <- v); - set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v); - set_int "tab_length" (fun v -> np.tab_length <- v); - set_bool "highlight_current_line" (fun v -> np.highlight_current_line <- v); - set_bool "nanoPG" (fun v -> np.nanoPG <- v); - () + Util.String.Map.iter iter m + +let pstring name p = string ~f:p#set name p#get +let pbool name p = bool ~f:p#set name p#get +let pmodifiers ?(all = false) name p = modifiers + ?allow:(if all then None else Some (str_to_mod_list modifiers_valid#get)) + ~f:(fun l -> p#set (mod_list_to_str l)) + ~help:"restart to apply" + name + (str_to_mod_list p#get) let configure ?(apply=(fun () -> ())) () = let cmd_coqtop = string - ~f:(fun s -> current.cmd_coqtop <- if s = "AUTO" then None else Some s) - " coqtop" (match current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in - let cmd_coqc = - string - ~f:(fun s -> current.cmd_coqc <- s) - " coqc" current.cmd_coqc in - let cmd_make = - string - ~f:(fun s -> current.cmd_make <- s) - " make" current.cmd_make in - let cmd_coqmakefile = - string - ~f:(fun s -> current.cmd_coqmakefile <- s) - "coqmakefile" current.cmd_coqmakefile in - let cmd_coqdoc = - string - ~f:(fun s -> current.cmd_coqdoc <- s) - " coqdoc" current.cmd_coqdoc in - let cmd_print = - string - ~f:(fun s -> current.cmd_print <- s) - " Print ps" current.cmd_print in + ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s)) + " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in + let cmd_coqc = pstring " coqc" cmd_coqc in + let cmd_make = pstring " make" cmd_make in + let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in + let cmd_coqdoc = pstring " coqdoc" cmd_coqdoc in + let cmd_print = pstring " Print ps" cmd_print in let config_font = let box = GPack.hbox () in @@ -435,18 +661,13 @@ let configure ?(apply=(fun () -> ())) () = "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; box#pack ~expand:true w#coerce; ignore (w#misc#connect#realize - ~callback:(fun () -> w#set_font_name - (Pango.Font.to_string current.text_font))); + ~callback:(fun () -> w#set_font_name text_font#get)); custom ~label:"Fonts for text" box (fun () -> let fd = w#font_name in - current.text_font <- (Pango.Font.from_string fd) ; -(* - Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string current.text_font); -*) - !refresh_editor_hook ()) + text_font#set fd) true in @@ -458,121 +679,94 @@ let configure ?(apply=(fun () -> ())) () = ~border_width:2 ~packing:(box#pack ~expand:true) () in - let background_label = GMisc.label - ~text:"Background color" - ~packing:(table#attach ~expand:`X ~left:0 ~top:0) () - in - let processed_label = GMisc.label - ~text:"Background color of processed text" - ~packing:(table#attach ~expand:`X ~left:0 ~top:1) () - in - let processing_label = GMisc.label - ~text:"Background color of text being processed" - ~packing:(table#attach ~expand:`X ~left:0 ~top:2) () - in - let error_label = GMisc.label - ~text:"Background color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:3) () - in - let error_fg_label = GMisc.label - ~text:"Foreground color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:4) () - in - let () = background_label#set_xalign 0. in - let () = processed_label#set_xalign 0. in - let () = processing_label#set_xalign 0. in - let () = error_label#set_xalign 0. in - let () = error_fg_label#set_xalign 0. in - let background_button = GButton.color_button - ~color:(Tags.color_of_string (current.background_color)) - ~packing:(table#attach ~left:1 ~top:0) () - in - let processed_button = GButton.color_button - ~color:(Tags.get_processed_color ()) - ~packing:(table#attach ~left:1 ~top:1) () - in - let processing_button = GButton.color_button - ~color:(Tags.get_processing_color ()) - ~packing:(table#attach ~left:1 ~top:2) () - in - let error_button = GButton.color_button - ~color:(Tags.get_error_color ()) - ~packing:(table#attach ~left:1 ~top:3) () - in - let error_fg_button = GButton.color_button - ~color:(Tags.get_error_fg_color ()) - ~packing:(table#attach ~left:1 ~top:4) () - in let reset_button = GButton.button ~label:"Reset" ~packing:box#pack () in - let reset_cb () = - background_button#set_color Tags.(color_of_string default_color); - processing_button#set_color Tags.(color_of_string default_processing_color); - processed_button#set_color Tags.(color_of_string default_processed_color); - error_button#set_color Tags.(color_of_string default_error_color); + let iter i (text, pref) = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) () + in + let () = label#set_xalign 0. in + let button = GButton.color_button + ~color:(Tags.color_of_string pref#get) + ~packing:(table#attach ~left:1 ~top:i) () + in + let _ = button#connect#color_set begin fun () -> + pref#set (Tags.string_of_color button#color) + end in + let reset _ = + pref#reset (); + button#set_color Tags.(color_of_string pref#get) + in + let _ = reset_button#connect#clicked ~callback:reset in + () in - let _ = reset_button#connect#clicked ~callback:reset_cb in + let () = Util.List.iteri iter [ + ("Background color", background_color); + ("Background color of processed text", processed_color); + ("Background color of text being processed", processing_color); + ("Background color of errors", error_color); + ("Foreground color of errors", error_fg_color); + ] in let label = "Color configuration" in - let callback () = - current.background_color <- Tags.string_of_color background_button#color; - current.processing_color <- Tags.string_of_color processing_button#color; - current.processed_color <- Tags.string_of_color processed_button#color; - current.error_color <- Tags.string_of_color error_button#color; - current.error_fg_color <- Tags.string_of_color error_fg_button#color; - !refresh_editor_hook (); - Tags.set_processing_color processing_button#color; - Tags.set_processed_color processed_button#color; - Tags.set_error_color error_button#color; - Tags.set_error_fg_color error_fg_button#color + let callback () = () in + custom ~label box callback true + in + + let config_tags = + let box = GPack.vbox () in + let scroll = GBin.scrolled_window + ~hpolicy:`NEVER + ~vpolicy:`AUTOMATIC + ~packing:(box#pack ~expand:true) + () in + let table = GPack.table + ~row_spacings:5 + ~col_spacings:5 + ~border_width:2 + ~packing:scroll#add_with_viewport () + in + let i = ref 0 in + let cb = ref [] in + let iter text tag = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) () + in + let () = label#set_xalign 0. in + let button = tag_button () in + let callback () = tag#set button#tag in + button#set_tag tag#get; + table#attach ~left:1 ~top:!i button#coerce; + incr i; + cb := callback :: !cb; + in + let () = Util.String.Map.iter iter !tags in + let label = "Tag configuration" in + let callback () = List.iter (fun f -> f ()) !cb in custom ~label box callback true in let config_editor = let label = "Editor configuration" in let box = GPack.vbox () in - let gen_button text active = - GButton.check_button ~label:text ~active ~packing:box#pack () in - let wrap = gen_button "Dynamic word wrap" current.dynamic_word_wrap in - let line = gen_button "Show line number" current.show_line_number in - let auto_indent = gen_button "Auto indentation" current.auto_indent in - let auto_complete = gen_button "Auto completion" current.auto_complete in - let show_spaces = gen_button "Show spaces" current.show_spaces in - let show_right_margin = gen_button "Show right margin" current.show_right_margin in - let show_progress_bar = gen_button "Show progress bar" current.show_progress_bar in - let spaces_instead_of_tabs = - gen_button "Insert spaces instead of tabs" - current.spaces_instead_of_tabs - in - let highlight_current_line = - gen_button "Highlight current line" - current.highlight_current_line - in - let nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" current.nanoPG in -(* let lbox = GPack.hbox ~packing:box#pack () in *) -(* let _ = GMisc.label ~text:"Tab width" *) -(* ~xalign:0. *) -(* ~packing:(lbox#pack ~expand:true) () *) -(* in *) -(* let tab_width = GEdit.spin_button *) -(* ~digits:0 ~packing:lbox#pack () *) -(* in *) - let callback () = - current.dynamic_word_wrap <- wrap#active; - current.show_line_number <- line#active; - current.auto_indent <- auto_indent#active; - current.show_spaces <- show_spaces#active; - current.show_right_margin <- show_right_margin#active; - current.show_progress_bar <- show_progress_bar#active; - current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active; - current.highlight_current_line <- highlight_current_line#active; - current.nanoPG <- nanoPG#active; - current.auto_complete <- auto_complete#active; -(* current.tab_length <- tab_width#value_as_int; *) - !refresh_editor_hook () + let button text (pref : bool preference) = + let active = pref#get in + let but = GButton.check_button ~label:text ~active ~packing:box#pack () in + ignore (but#connect#toggled (fun () -> pref#set but#active)) in + let () = button "Dynamic word wrap" dynamic_word_wrap in + let () = button "Show line number" show_line_number in + let () = button "Auto indentation" auto_indent in + let () = button "Auto completion" auto_complete in + let () = button "Show spaces" show_spaces in + let () = button "Show right margin" show_right_margin in + let () = button "Show progress bar" show_progress_bar in + let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in + let () = button "Highlight current line" highlight_current_line in + let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let callback () = () in custom ~label box callback true in @@ -600,177 +794,110 @@ let configure ?(apply=(fun () -> ())) () = (string_of_int current.window_width) in *) -(* let use_utf8_notation = - bool - ~f:(fun b -> - current.use_utf8_notation <- b; - ) - "Use Unicode Notation: " current.use_utf8_notation - in -*) (* let config_appearance = [show_toolbar; window_width; window_height] in *) - let global_auto_revert = - bool - ~f:(fun s -> current.global_auto_revert <- s) - "Enable global auto revert" current.global_auto_revert - in + let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in let global_auto_revert_delay = string - ~f:(fun s -> current.global_auto_revert_delay <- + ~f:(fun s -> global_auto_revert_delay#set (try int_of_string s with _ -> 10000)) "Global auto revert delay (ms)" - (string_of_int current.global_auto_revert_delay) + (string_of_int global_auto_revert_delay#get) in - let auto_save = - bool - ~f:(fun s -> current.auto_save <- s) - "Enable auto save" current.auto_save - in + let auto_save = pbool "Enable auto save" auto_save in let auto_save_delay = string - ~f:(fun s -> current.auto_save_delay <- + ~f:(fun s -> auto_save_delay#set (try int_of_string s with _ -> 10000)) "Auto save delay (ms)" - (string_of_int current.auto_save_delay) + (string_of_int auto_save_delay#get) in - let stop_before = - bool - ~f:(fun s -> current.stop_before <- s) - "Stop interpreting before the current point" current.stop_before - in + let stop_before = pbool "Stop interpreting before the current point" stop_before in - let reset_on_tab_switch = - bool - ~f:(fun s -> current.reset_on_tab_switch <- s) - "Reset coqtop on tab switch" current.reset_on_tab_switch - in + let reset_on_tab_switch = pbool "Reset coqtop on tab switch" reset_on_tab_switch in - let vertical_tabs = - bool - ~f:(fun s -> current.vertical_tabs <- s; !refresh_tabs_hook ()) - "Vertical tabs" current.vertical_tabs - in + let vertical_tabs = pbool "Vertical tabs" vertical_tabs in - let opposite_tabs = - bool - ~f:(fun s -> current.opposite_tabs <- s; !refresh_tabs_hook ()) - "Tabs on opposite side" current.opposite_tabs - in + let opposite_tabs = pbool "Tabs on opposite side" opposite_tabs in let encodings = combo "File charset encoding " - ~f:(fun s -> current.encoding <- (inputenc_of_string s)) + ~f:(fun s -> encoding#set (inputenc_of_string s)) ~new_allowed: true - ("UTF-8"::"LOCALE":: match current.encoding with + ("UTF-8"::"LOCALE":: match encoding#get with |Emanual s -> [s] |_ -> [] ) - (string_of_inputenc current.encoding) + (string_of_inputenc encoding#get) + in + + let line_ending = + combo + "EOL character" + ~f:(fun s -> line_ending#set (line_end_of_string s)) + ~new_allowed:false + ["unix"; "windows"; "default"] + (line_end_to_string line_ending#get) in let source_style = - let f s = - current.source_style <- s; - !refresh_style_hook () - in combo "Highlighting style:" - ~f ~new_allowed:false - style_manager#style_scheme_ids current.source_style + ~f:source_style#set ~new_allowed:false + style_manager#style_scheme_ids source_style#get in let source_language = - let f s = - current.source_language <- s; - !refresh_language_hook () - in combo "Language:" - ~f ~new_allowed:false + ~f:source_language#set ~new_allowed:false (List.filter (fun x -> Str.string_match (Str.regexp "^coq") x 0) lang_manager#language_ids) - current.source_language + source_language#get in let read_project = combo "Project file options are" - ~f:(fun s -> current.read_project <- project_behavior_of_string s) + ~f:(fun s -> read_project#set (project_behavior_of_string s)) ~editable:false [string_of_project_behavior Subst_args; string_of_project_behavior Append_args; string_of_project_behavior Ignore_args] - (string_of_project_behavior current.read_project) - in - let project_file_name = - string "Default name for project file" - ~f:(fun s -> current.project_file_name <- s) - current.project_file_name + (string_of_project_behavior read_project#get) in - let help_string = - "restart to apply" - in - let the_valid_mod = str_to_mod_list current.modifiers_valid in + let project_file_name = pstring "Default name for project file" project_file_name in let modifier_for_tactics = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l) - ~help:help_string - "Modifiers for Tactics Menu" - (str_to_mod_list current.modifier_for_tactics) + pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics in let modifier_for_templates = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l) - ~help:help_string - "Modifiers for Templates Menu" - (str_to_mod_list current.modifier_for_templates) + pmodifiers "Modifiers for Templates Menu" modifier_for_templates in let modifier_for_navigation = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l) - ~help:help_string - "Modifiers for Navigation Menu" - (str_to_mod_list current.modifier_for_navigation) + pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation in let modifier_for_display = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l) - ~help:help_string - "Modifiers for View Menu" - (str_to_mod_list current.modifier_for_display) + pmodifiers "Modifiers for View Menu" modifier_for_display in - let modifiers_valid = - modifiers - ~f:(fun l -> - current.modifiers_valid <- mod_list_to_str l) - "Allowed modifiers" - the_valid_mod + let modifier_for_queries = + pmodifiers "Modifiers for Queries Menu" modifier_for_queries in - let modifier_notice = - let b = GPack.hbox () in - let _lbl = - GMisc.label ~markup:"You need to restart CoqIDE after changing these settings" - ~packing:b#add () in - custom b (fun () -> ()) true + let modifiers_valid = + pmodifiers ~all:true "Allowed modifiers" modifiers_valid in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo ~help:"(%s for file name)" "External editor" - ~f:(fun s -> current.cmd_editor <- s) + ~f:cmd_editor#set ~new_allowed: true - (predefined@[if List.mem current.cmd_editor predefined then "" - else current.cmd_editor]) - current.cmd_editor + (predefined@[if List.mem cmd_editor#get predefined then "" + else cmd_editor#get]) + cmd_editor#get in let cmd_browse = let predefined = [ @@ -783,58 +910,82 @@ let configure ?(apply=(fun () -> ())) () = combo ~help:"(%s for url)" "Browser" - ~f:(fun s -> current.cmd_browse <- s) + ~f:cmd_browse#set ~new_allowed: true - (predefined@[if List.mem current.cmd_browse predefined then "" - else current.cmd_browse]) - current.cmd_browse + (predefined@[if List.mem cmd_browse#get predefined then "" + else cmd_browse#get]) + cmd_browse#get in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in combo "Manual URL" - ~f:(fun s -> current.doc_url <- s) + ~f:doc_url#set ~new_allowed: true - (predefined@[if List.mem current.doc_url predefined then "" - else current.doc_url]) - current.doc_url in + (predefined@[if List.mem doc_url#get predefined then "" + else doc_url#get]) + doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo "Library URL" - ~f:(fun s -> current.library_url <- s) + ~f:(fun s -> library_url#set s) ~new_allowed: true - (predefined@[if List.mem current.library_url predefined then "" - else current.library_url]) - current.library_url + (predefined@[if List.mem library_url#get predefined then "" + else library_url#get]) + library_url#get in let automatic_tactics = strings - ~f:(fun l -> current.automatic_tactics <- l) + ~f:automatic_tactics#set ~add:(fun () -> [""]) "Wizard tactics to try in order" - current.automatic_tactics + automatic_tactics#get in - let contextual_menus_on_goal = - bool - ~f:(fun s -> - current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal_hook s) - "Contextual menus on goal" current.contextual_menus_on_goal - in + let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch; vertical_tabs;opposite_tabs] in + let add_user_query () = + let input_string l v = + match GToolbox.input_string ~title:l v with + | None -> "" + | Some s -> s + in + let q = input_string "User query" "Your query" in + let k = input_string "Shortcut key" "Shortcut (a single letter)" in + let q = CString.map (fun c -> if c = '$' then ' ' else c) q in + (* Anything that is not a simple letter will be ignored. *) + let k = + if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k + else "" in + let k = CString.uppercase k in + [q, k] + in + + let user_queries = + list + ~f:user_queries#set + (* Disallow same query, key or empty query. *) + ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "" || q1 = q2) + ~add:add_user_query + ~titles:["User query"; "Shortcut key"] + "User queries" + (fun (q, s) -> [q; s]) + user_queries#get + + in + (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = @@ -842,11 +993,13 @@ let configure ?(apply=(fun () -> ())) () = [config_font]); Section("Colors", Some `SELECT_COLOR, [config_color; source_language; source_style]); + Section("Tags", Some `SELECT_COLOR, + [config_tags]); Section("Editor", Some `EDIT, [config_editor]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings; + encodings; line_ending; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; @@ -862,9 +1015,10 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation; modifier_notice]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; + modifier_for_queries; user_queries]); Section("Misc", Some `ADD, - misc)] + misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); -- cgit v1.2.3