diff options
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r-- | ide/preferences.ml | 233 |
1 files changed, 124 insertions, 109 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 790bf560..02673098 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,53 +1,44 @@ (************************************************************************) (* 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-2010 *) (* \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 System.home ".coqide.keys" +let accel_file = Filename.concat Minilib.xdg_config_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>" + | `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 pref = { @@ -63,6 +54,9 @@ type pref = mutable auto_save_delay : int; mutable auto_save_name : string * string; + mutable read_project : project_behavior; + mutable project_file_name : string; + mutable encoding_use_locale : bool; mutable encoding_use_utf8 : bool; mutable encoding_manual : string; @@ -70,11 +64,11 @@ type pref = 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; @@ -117,6 +111,9 @@ let (current:pref ref) = auto_save_delay = 10000; auto_save_name = "#","#"; + read_project = Ignore_args; + project_file_name = "_CoqProject"; + encoding_use_locale = true; encoding_use_utf8 = false; encoding_manual = "ISO_8859-1"; @@ -124,18 +121,20 @@ let (current:pref ref) = 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; @@ -168,13 +167,15 @@ let contextual_menus_on_goal = ref (fun x -> ()) let resize_window = ref (fun () -> ()) let save_pref () = + if not (Sys.file_exists Minilib.xdg_config_home) + then Unix.mkdir Minilib.xdg_config_home 0o700; (try GtkData.AccelMap.save accel_file with _ -> ()); 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_coqc" [p.cmd_coqc] ++ add "cmd_make" [p.cmd_make] ++ add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ @@ -186,22 +187,20 @@ 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 "project_options" [string_of_project_behavior p.read_project] ++ + add "project_file_name" [p.project_file_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 "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] ++ @@ -222,15 +221,17 @@ let save_pref () = add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ Config_lexer.print_file pref_file - with _ -> prerr_endline "Could not save preferences." let load_pref () = - (try GtkData.AccelMap.load accel_file with _ -> ()); + let accel_dir = List.find + (fun x -> Sys.file_exists (Filename.concat x "coqide.keys")) + Minilib.xdg_config_dirs in + GtkData.AccelMap.load (Filename.concat accel_dir "coqide.keys"); let p = !current in - try + let m = Config_lexer.load_file 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 @@ -251,19 +252,22 @@ let load_pref () = 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 "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 +278,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); @@ -289,21 +293,10 @@ let load_pref () = 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; + 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_coqc = @@ -462,46 +455,62 @@ let configure ?(apply=(fun () -> ())) () = (if !current.encoding_use_utf8 then "UTF-8" else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) 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 +529,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 +542,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 +555,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 @@ -577,27 +589,30 @@ let configure ?(apply=(fun () -> ())) () = (* 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("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", + Section("Externals", None, [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; cmd_editor; cmd_browse;doc_url;library_url]); - Section("Tactics Wizard", + 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 (* |