diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 437 |
1 files changed, 266 insertions, 171 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 790bf560..2fb5023f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,56 +1,88 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Configwin open Printf -open Util -let pref_file = Filename.concat System.home ".coqiderc" +let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc" +let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys" + +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.xdg_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 Minilib.home ".coqiderc" -let accel_file = Filename.concat System.home ".coqide.keys" +let loaded_accel_file = + try get_config_file "coqide.keys" + with Not_found -> Filename.concat Minilib.home ".coqide.keys" let mod_to_str (m:Gdk.Tags.modifier) = match m with - | `MOD1 -> "MOD1" - | `MOD2 -> "MOD2" - | `MOD3 -> "MOD3" - | `MOD4 -> "MOD4" - | `MOD5 -> "MOD5" - | `BUTTON1 -> "BUTTON1" - | `BUTTON2 -> "BUTTON2" - | `BUTTON3 -> "BUTTON3" - | `BUTTON4 -> "BUTTON4" - | `BUTTON5 -> "BUTTON5" - | `CONTROL -> "CONTROL" - | `LOCK -> "LOCK" - | `SHIFT -> "SHIFT" - -let (str_to_mod:string -> Gdk.Tags.modifier) = - function - | "MOD1" -> `MOD1 - | "MOD2" -> `MOD2 - | "MOD3" -> `MOD3 - | "MOD4" -> `MOD4 - | "MOD5" -> `MOD5 - | "BUTTON1" -> `BUTTON1 - | "BUTTON2" -> `BUTTON2 - | "BUTTON3" -> `BUTTON3 - | "BUTTON4" -> `BUTTON4 - | "BUTTON5" -> `BUTTON5 - | "CONTROL" -> `CONTROL - | "LOCK" -> `LOCK - | "SHIFT" -> `SHIFT - | s -> `MOD1 + | `MOD1 -> "<Alt>" + | `MOD2 -> "<Mod2>" + | `MOD3 -> "<Mod3>" + | `MOD4 -> "<Mod4>" + | `MOD5 -> "<Mod5>" + | `CONTROL -> "<Control>" + | `SHIFT -> "<Shift>" + | `HYPER -> "<Hyper>" + | `META -> "<Meta>" + | `RELEASE -> "" + | `SUPER -> "<Super>" + | `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> "" + +let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l + +let str_to_mod_list s = snd (GtkData.AccelGroup.parse s) + +type project_behavior = Ignore_args | Append_args | Subst_args + +let string_of_project_behavior = function + |Ignore_args -> "ignored" + |Append_args -> "appended to arguments" + |Subst_args -> "taken instead of arguments" + +let project_behavior_of_string s = + if s = "taken instead of arguments" then Subst_args + else if s = "appended to arguments" then Append_args + else Ignore_args + +type inputenc = Elocale | Eutf8 | Emanual of string + +let string_of_inputenc = function + |Elocale -> "LOCALE" + |Eutf8 -> "UTF-8" + |Emanual s -> s + +let inputenc_of_string s = + (if s = "UTF-8" then Eutf8 + else if s = "LOCALE" then Elocale + else Emanual s) + + +(** Hooks *) + +let refresh_font_hook = ref (fun () -> ()) +let refresh_background_color_hook = ref (fun () -> ()) +let refresh_toolbar_hook = ref (fun () -> ()) +let auto_complete_hook = ref (fun x -> ()) +let contextual_menus_on_goal_hook = ref (fun x -> ()) +let resize_window_hook = ref (fun () -> ()) +let refresh_tabs_hook = ref (fun () -> ()) type pref = { + mutable cmd_coqtop : string option; mutable cmd_coqc : string; mutable cmd_make : string; mutable cmd_coqmakefile : string; @@ -63,18 +95,19 @@ type pref = mutable auto_save_delay : int; mutable auto_save_name : string * string; - mutable encoding_use_locale : bool; - mutable encoding_use_utf8 : bool; - mutable encoding_manual : string; + mutable read_project : project_behavior; + mutable project_file_name : string; + + mutable encoding : inputenc; mutable automatic_tactics : string list; mutable cmd_print : string; - mutable modifier_for_navigation : Gdk.Tags.modifier list; - mutable modifier_for_templates : Gdk.Tags.modifier list; - mutable modifier_for_tactics : Gdk.Tags.modifier list; - mutable modifier_for_display : Gdk.Tags.modifier list; - mutable modifiers_valid : Gdk.Tags.modifier list; + mutable modifier_for_navigation : string; + mutable modifier_for_templates : string; + mutable modifier_for_tactics : string; + mutable modifier_for_display : string; + mutable modifiers_valid : string; mutable cmd_browse : string; mutable cmd_editor : string; @@ -95,15 +128,20 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; + + mutable background_color : string; + mutable processing_color : string; + mutable processed_color : string; + } let use_default_doc_url = "(automatic)" let (current:pref ref) = ref { + cmd_coqtop = None; cmd_coqc = "coqc"; cmd_make = "make"; cmd_coqmakefile = "coq_makefile -o makefile *.v"; @@ -117,25 +155,28 @@ let (current:pref ref) = auto_save_delay = 10000; auto_save_name = "#","#"; - encoding_use_locale = true; - encoding_use_utf8 = false; - encoding_manual = "ISO_8859-1"; + read_project = Ignore_args; + project_file_name = "_CoqProject"; + + encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; - modifier_for_navigation = [`CONTROL; `MOD1]; - modifier_for_templates = [`CONTROL; `SHIFT]; - modifier_for_tactics = [`CONTROL; `MOD1]; - modifier_for_display = [`MOD1;`SHIFT]; - modifiers_valid = [`SHIFT; `CONTROL; `MOD1]; + modifier_for_navigation = "<Control><Alt>"; + modifier_for_templates = "<Control><Shift>"; + modifier_for_tactics = "<Control><Alt>"; + modifier_for_display = "<Alt><Shift>"; + modifiers_valid = "<Alt><Control><Shift>"; cmd_browse = Flags.browser_cmd_fmt; cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s"; (* text_font = Pango.Font.from_string "sans 12";*) - text_font = Pango.Font.from_string "Monospace 10"; + text_font = Pango.Font.from_string (match Coq_config.gtk_platform with + |`QUARTZ -> "Arial Unicode MS 11" + |_ -> "Monospace 10"); doc_url = Coq_config.wwwrefman; library_url = Coq_config.wwwstdlib; @@ -151,30 +192,25 @@ let (current:pref ref) = *) auto_complete = false; stop_before = true; - lax_syntax = true; vertical_tabs = false; opposite_tabs = false; - } - - -let change_font = ref (fun f -> ()) -let show_toolbar = ref (fun x -> ()) + background_color = "cornsilk"; + processed_color = "light green"; + processing_color = "light blue"; -let auto_complete = ref (fun x -> ()) - -let contextual_menus_on_goal = ref (fun x -> ()) - -let resize_window = ref (fun () -> ()) + } let save_pref () = - (try GtkData.AccelMap.save accel_file - with _ -> ()); + if not (Sys.file_exists Minilib.xdg_config_home) + then Unix.mkdir Minilib.xdg_config_home 0o700; + let () = try GtkData.AccelMap.save accel_file with _ -> () in let p = !current in - try - let add = Stringmap.add in + + let add = Minilib.Stringmap.add in let (++) x f = f x in - Stringmap.empty ++ + Minilib.Stringmap.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] ++ @@ -186,22 +222,18 @@ let save_pref () = 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 "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++ - add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++ - add "encoding_manual" [p.encoding_manual] ++ + add "project_options" [string_of_project_behavior p.read_project] ++ + add "project_file_name" [p.project_file_name] ++ + + add "encoding" [string_of_inputenc p.encoding] ++ add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ - add "modifier_for_navigation" - (List.map mod_to_str p.modifier_for_navigation) ++ - add "modifier_for_templates" - (List.map mod_to_str p.modifier_for_templates) ++ - add "modifier_for_tactics" - (List.map mod_to_str p.modifier_for_tactics) ++ - add "modifier_for_display" - (List.map mod_to_str p.modifier_for_display) ++ - add "modifiers_valid" - (List.map mod_to_str p.modifiers_valid) ++ + 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] ++ @@ -218,19 +250,20 @@ let save_pref () = 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 "lax_syntax" [string_of_bool p.lax_syntax] ++ 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] ++ Config_lexer.print_file pref_file - with _ -> prerr_endline "Could not save preferences." let load_pref () = - (try GtkData.AccelMap.load accel_file with _ -> ()); + let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let p = !current in - try - let m = Config_lexer.load_file pref_file in + + let m = Config_lexer.load_file loaded_pref_file in let np = { p with cmd_coqc = p.cmd_coqc } in - let set k f = try let v = Stringmap.find k m in f v with _ -> () in + let set k f = try let v = Minilib.Stringmap.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 @@ -238,6 +271,8 @@ let load_pref () = let set_command_with_pair_compat k f = set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) 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); @@ -248,22 +283,23 @@ let load_pref () = 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_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v); - set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v); - set_hd "encoding_manual" (fun v -> np.encoding_manual <- v); + 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 "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); - set "modifier_for_navigation" - (fun v -> np.modifier_for_navigation <- List.map str_to_mod v); - set "modifier_for_templates" - (fun v -> np.modifier_for_templates <- List.map str_to_mod v); - set "modifier_for_tactics" - (fun v -> np.modifier_for_tactics <- List.map str_to_mod v); - set "modifier_for_display" - (fun v -> np.modifier_for_display <- List.map str_to_mod v); - set "modifiers_valid" - (fun v -> np.modifiers_valid <- List.map str_to_mod 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); @@ -274,7 +310,7 @@ let load_pref () = v <> Coq_config.wwwcoq ^ "doc" && v <> Coq_config.wwwcoq ^ "doc/" then - prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v); + (*prerr_endline ("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); @@ -286,26 +322,21 @@ let load_pref () = 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 "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); - current := np; + 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); + current := np (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - with e -> - prerr_endline ("Could not load preferences ("^ - (Printexc.to_string e)^").") - -let split_string_format s = - try - let i = Util.string_index_from s 0 "%s" in - let pre = (String.sub s 0 i) in - let post = String.sub s (i+2) (String.length s - i - 2) in - pre,post - with Not_found -> s,"" 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) @@ -332,7 +363,7 @@ let configure ?(apply=(fun () -> ())) () = let w = GMisc.font_selection () in w#set_preview_text "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; - box#pack w#coerce; + box#pack ~expand:true w#coerce; ignore (w#misc#connect#realize ~callback:(fun () -> w#set_font_name (Pango.Font.to_string !current.text_font))); @@ -345,9 +376,67 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - !change_font !current.text_font) + !refresh_font_hook ()) true in + + let config_color = + let box = GPack.vbox () in + let table = GPack.table + ~row_spacings:5 + ~col_spacings:5 + ~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 () = background_label#set_xalign 0. in + let () = processed_label#set_xalign 0. in + let () = processing_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 reset_button = GButton.button + ~label:"Reset" + ~packing:box#pack () + in + let reset_cb () = + background_button#set_color (Tags.color_of_string "cornsilk"); + processing_button#set_color (Tags.color_of_string "light blue"); + processed_button#set_color (Tags.color_of_string "light green"); + in + let _ = reset_button#connect#clicked ~callback:reset_cb 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; + !refresh_background_color_hook (); + Tags.set_processing_color processing_button#color; + Tags.set_processed_color processed_button#color + in + custom ~label box callback true + in + (* let show_toolbar = bool @@ -376,7 +465,7 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.auto_complete <- s; - !auto_complete s) + !auto_complete_hook s) "Auto Complete" !current.auto_complete in @@ -423,85 +512,85 @@ let configure ?(apply=(fun () -> ())) () = "Stop interpreting before the current point" !current.stop_before in - let lax_syntax = - bool - ~f:(fun s -> !current.lax_syntax <- s) - "Relax read-only constraint at end of command" !current.lax_syntax - in - let vertical_tabs = bool - ~f:(fun s -> !current.vertical_tabs <- s) + ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ()) "Vertical tabs" !current.vertical_tabs in let opposite_tabs = bool - ~f:(fun s -> !current.opposite_tabs <- s) + ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ()) "Tabs on opposite side" !current.opposite_tabs in let encodings = combo "File charset encoding " - ~f:(fun s -> - match s with - | "UTF-8" -> - !current.encoding_use_utf8 <- true; - !current.encoding_use_locale <- false - | "LOCALE" -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- true - | _ -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- false; - !current.encoding_manual <- s; - ) + ~f:(fun s -> !current.encoding <- (inputenc_of_string s)) ~new_allowed: true - ["UTF-8";"LOCALE";!current.encoding_manual] - (if !current.encoding_use_utf8 then "UTF-8" - else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) + ("UTF-8"::"LOCALE":: match !current.encoding with + |Emanual s -> [s] + |_ -> [] + ) + (string_of_inputenc !current.encoding) + in + let read_project = + combo + "Project file options are" + ~f:(fun s -> !current.read_project <- 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 in let help_string = "restart to apply" in + let the_valid_mod = str_to_mod_list !current.modifiers_valid in let modifier_for_tactics = modifiers - ~allow:!current.modifiers_valid - ~f:(fun l -> !current.modifier_for_tactics <- l) + ~allow:the_valid_mod + ~f:(fun l -> !current.modifier_for_tactics <- mod_list_to_str l) ~help:help_string "Modifiers for Tactics Menu" - !current.modifier_for_tactics + (str_to_mod_list !current.modifier_for_tactics) in let modifier_for_templates = modifiers - ~allow:!current.modifiers_valid - ~f:(fun l -> !current.modifier_for_templates <- l) + ~allow:the_valid_mod + ~f:(fun l -> !current.modifier_for_templates <- mod_list_to_str l) ~help:help_string "Modifiers for Templates Menu" - !current.modifier_for_templates + (str_to_mod_list !current.modifier_for_templates) in let modifier_for_navigation = modifiers - ~allow:!current.modifiers_valid - ~f:(fun l -> !current.modifier_for_navigation <- l) + ~allow:the_valid_mod + ~f:(fun l -> !current.modifier_for_navigation <- mod_list_to_str l) ~help:help_string "Modifiers for Navigation Menu" - !current.modifier_for_navigation + (str_to_mod_list !current.modifier_for_navigation) in let modifier_for_display = modifiers - ~allow:!current.modifiers_valid - ~f:(fun l -> !current.modifier_for_display <- l) + ~allow:the_valid_mod + ~f:(fun l -> !current.modifier_for_display <- mod_list_to_str l) ~help:help_string "Modifiers for Display Menu" - !current.modifier_for_display + (str_to_mod_list !current.modifier_for_display) in let modifiers_valid = modifiers - ~f:(fun l -> !current.modifiers_valid <- l) + ~f:(fun l -> !current.modifiers_valid <- mod_list_to_str l) "Allowed modifiers" - !current.modifiers_valid + the_valid_mod in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in @@ -520,8 +609,7 @@ let configure ?(apply=(fun () -> ())) () = "netscape -remote \"openURL(%s)\""; "mozilla -remote \"openURL(%s)\""; "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &"; - "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"; - "open -a Safari %s &" + "seamonkey -remote \"openURL(%s)\" || seamonkey %s &" ] in combo ~help:"(%s for url)" @@ -534,6 +622,8 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]); + Coq_config.wwwrefman; use_default_doc_url ] in combo @@ -545,11 +635,13 @@ let configure ?(apply=(fun () -> ())) () = !current.doc_url in let library_url = let predefined = [ + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]); Coq_config.wwwstdlib ] in combo "Library URL" ~f:(fun s -> !current.library_url <- s) + ~new_allowed: true (predefined@[if List.mem !current.library_url predefined then "" else !current.library_url]) !current.library_url @@ -567,43 +659,46 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + !contextual_menus_on_goal_hook s) "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; + let misc = [contextual_menus_on_goal;auto_complete;stop_before; vertical_tabs;opposite_tabs] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = - [Section("Fonts", + [Section("Fonts", Some `SELECT_FONT, [config_font]); - Section("Files", + Section("Colors", Some `SELECT_COLOR, [config_color]); + Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) encodings; ]); + Section("Project", Some (`STOCK "gtk-page-setup"), + [project_file_name;read_project; + ]); (* Section("Appearance", config_appearance); *) - Section("Externals", - [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; - cmd_editor; - cmd_browse;doc_url;library_url]); - Section("Tactics Wizard", + Section("Externals", None, + [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; + cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); + Section("Tactics Wizard", None, [automatic_tactics]); - Section("Shortcuts", + Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation]); - Section("Misc", + Section("Misc", Some `ADD, misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - let x = edit ~apply ~width:500 "Customizations" cmds in + let x = edit ~apply "Customizations" cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) |