From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- ide/preferences.ml | 291 ++++++++++++++++++++++++++++------------------------- 1 file changed, 156 insertions(+), 135 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index ffb346d9..4e87d1df 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 12104 2009-04-24 18:10:10Z notin $ *) +(* $Id$ *) open Configwin open Printf @@ -16,7 +16,7 @@ let pref_file = Filename.concat System.home ".coqiderc" let accel_file = Filename.concat System.home ".coqide.keys" -let mod_to_str (m:Gdk.Tags.modifier) = +let mod_to_str (m:Gdk.Tags.modifier) = match m with | `MOD1 -> "MOD1" | `MOD2 -> "MOD2" @@ -34,19 +34,19 @@ let mod_to_str (m:Gdk.Tags.modifier) = 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 + | "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 type pref = @@ -100,7 +100,9 @@ type pref = mutable opposite_tabs : bool; } -let (current:pref ref) = +let use_default_doc_url = "(automatic)" + +let (current:pref ref) = ref { cmd_coqc = "coqc"; cmd_make = "make"; @@ -110,38 +112,38 @@ let (current:pref ref) = global_auto_revert = false; global_auto_revert_delay = 10000; - + auto_save = true; auto_save_delay = 10000; auto_save_name = "#","#"; - + encoding_use_locale = true; encoding_use_utf8 = false; encoding_manual = "ISO_8859-1"; 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]; - + 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"; doc_url = Coq_config.wwwrefman; library_url = Coq_config.wwwstdlib; - + show_toolbar = true; contextual_menus_on_goal = true; window_width = 800; - window_height = 600; + window_height = 600; query_window_width = 600; query_window_height = 400; (* @@ -166,10 +168,10 @@ let contextual_menus_on_goal = ref (fun x -> ()) let resize_window = ref (fun () -> ()) let save_pref () = - (try GtkData.AccelMap.save accel_file + (try GtkData.AccelMap.save accel_file with _ -> ()); let p = !current in - try + try let add = Stringmap.add in let (++) x f = f x in Stringmap.empty ++ @@ -178,7 +180,7 @@ let save_pref () = add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ add "cmd_coqdoc" [p.cmd_coqdoc] ++ add "global_auto_revert" [string_of_bool p.global_auto_revert] ++ - add "global_auto_revert_delay" + 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] ++ @@ -190,15 +192,15 @@ let save_pref () = add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ - add "modifier_for_navigation" + add "modifier_for_navigation" (List.map mod_to_str p.modifier_for_navigation) ++ - add "modifier_for_templates" + add "modifier_for_templates" (List.map mod_to_str p.modifier_for_templates) ++ - add "modifier_for_tactics" + add "modifier_for_tactics" (List.map mod_to_str p.modifier_for_tactics) ++ - add "modifier_for_display" + add "modifier_for_display" (List.map mod_to_str p.modifier_for_display) ++ - add "modifiers_valid" + add "modifiers_valid" (List.map mod_to_str p.modifiers_valid) ++ add "cmd_browse" [p.cmd_browse] ++ add "cmd_editor" [p.cmd_editor] ++ @@ -208,7 +210,7 @@ let save_pref () = 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" + 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] ++ @@ -221,12 +223,11 @@ let save_pref () = 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 p = !current in - try + 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 @@ -234,7 +235,7 @@ let load_pref () = 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 = + let set_command_with_pair_compat k f = set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) in set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); @@ -242,7 +243,7 @@ let load_pref () = set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v); set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v); - set_int "global_auto_revert_delay" + 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); @@ -253,23 +254,26 @@ let load_pref () = set "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); - set "modifier_for_navigation" + set "modifier_for_navigation" (fun v -> np.modifier_for_navigation <- List.map str_to_mod v); - set "modifier_for_templates" + set "modifier_for_templates" (fun v -> np.modifier_for_templates <- List.map str_to_mod v); - set "modifier_for_tactics" + set "modifier_for_tactics" (fun v -> np.modifier_for_tactics <- List.map str_to_mod v); - set "modifier_for_display" + set "modifier_for_display" (fun v -> np.modifier_for_display <- List.map str_to_mod v); - set "modifiers_valid" + set "modifiers_valid" (fun v -> np.modifiers_valid <- List.map str_to_mod 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 -> np.doc_url <- v); + set_hd "doc_url" (fun v -> + if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url then + 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); - set_bool "contextual_menus_on_goal" + 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); @@ -284,38 +288,38 @@ let load_pref () = (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - with e -> + with e -> prerr_endline ("Could not load preferences ("^ (Printexc.to_string e)^").") - + let split_string_format s = - try + 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 = +let configure ?(apply=(fun () -> ())) () = + let cmd_coqc = string - ~f:(fun s -> !current.cmd_coqc <- s) + ~f:(fun s -> !current.cmd_coqc <- s) " coqc" !current.cmd_coqc in - let cmd_make = - string + let cmd_make = + string ~f:(fun s -> !current.cmd_make <- s) " make" !current.cmd_make in - let cmd_coqmakefile = - string + let cmd_coqmakefile = + string ~f:(fun s -> !current.cmd_coqmakefile <- s) "coqmakefile" !current.cmd_coqmakefile in - let cmd_coqdoc = - string + 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) + let cmd_print = + string + ~f:(fun s -> !current.cmd_print <- s) " Print ps" !current.cmd_print in let config_font = @@ -324,15 +328,15 @@ let configure ?(apply=(fun () -> ())) () = w#set_preview_text "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; box#pack w#coerce; - ignore (w#misc#connect#realize - ~callback:(fun () -> w#set_font_name + ignore (w#misc#connect#realize + ~callback:(fun () -> w#set_font_name (Pango.Font.to_string !current.text_font))); custom ~label:"Fonts for text" box - (fun () -> + (fun () -> let fd = w#font_name in - !current.text_font <- (Pango.Font.from_string fd) ; + !current.text_font <- (Pango.Font.from_string fd) ; (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) @@ -340,80 +344,80 @@ let configure ?(apply=(fun () -> ())) () = true in (* - let show_toolbar = - bool - ~f:(fun s -> - !current.show_toolbar <- s; - !show_toolbar s) + let show_toolbar = + bool + ~f:(fun s -> + !current.show_toolbar <- s; + !show_toolbar s) "Show toolbar" !current.show_toolbar in let window_height = string ~f:(fun s -> !current.window_height <- (try int_of_string s with _ -> 600); !resize_window (); - ) - "Window height" + ) + "Window height" (string_of_int !current.window_height) - in + in let window_width = string - ~f:(fun s -> !current.window_width <- - (try int_of_string s with _ -> 800)) - "Window width" + ~f:(fun s -> !current.window_width <- + (try int_of_string s with _ -> 800)) + "Window width" (string_of_int !current.window_width) - in + in *) - let auto_complete = - bool - ~f:(fun s -> - !current.auto_complete <- s; - !auto_complete s) + let auto_complete = + bool + ~f:(fun s -> + !current.auto_complete <- s; + !auto_complete s) "Auto Complete" !current.auto_complete in -(* let use_utf8_notation = - bool - ~f:(fun b -> +(* 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) + 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_delay = string - ~f:(fun s -> !current.global_auto_revert_delay <- - (try int_of_string s with _ -> 10000)) - "Global auto revert delay (ms)" + ~f:(fun s -> !current.global_auto_revert_delay <- + (try int_of_string s with _ -> 10000)) + "Global auto revert delay (ms)" (string_of_int !current.global_auto_revert_delay) - in + in - let auto_save = - bool - ~f:(fun s -> !current.auto_save <- s) + let auto_save = + bool + ~f:(fun s -> !current.auto_save <- s) "Enable auto save" !current.auto_save in let auto_save_delay = string - ~f:(fun s -> !current.auto_save_delay <- - (try int_of_string s with _ -> 10000)) - "Auto save delay (ms)" + ~f:(fun s -> !current.auto_save_delay <- + (try int_of_string s with _ -> 10000)) + "Auto save delay (ms)" (string_of_int !current.auto_save_delay) - in + in let stop_before = bool ~f:(fun s -> !current.stop_before <- s) "Stop interpreting before the current point" !current.stop_before in - + let lax_syntax = bool ~f:(fun s -> !current.lax_syntax <- s) @@ -432,31 +436,31 @@ let configure ?(apply=(fun () -> ())) () = "Tabs on opposite side" !current.opposite_tabs in - let encodings = - combo + let encodings = + combo "File charset encoding " - ~f:(fun s -> + ~f:(fun s -> match s with - | "UTF-8" -> + | "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; ) ~new_allowed: true ["UTF-8";"LOCALE";!current.encoding_manual] - (if !current.encoding_use_utf8 then "UTF-8" + (if !current.encoding_use_utf8 then "UTF-8" else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) in - let help_string = - "Press a set of modifiers and an extra key together (needs then a restart to apply!)" + let help_string = + "restart to apply" in - let modifier_for_tactics = + let modifier_for_tactics = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_tactics <- l) @@ -464,7 +468,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Tactics Menu" !current.modifier_for_tactics in - let modifier_for_templates = + let modifier_for_templates = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_templates <- l) @@ -472,7 +476,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Templates Menu" !current.modifier_for_templates in - let modifier_for_navigation = + let modifier_for_navigation = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_navigation <- l) @@ -480,7 +484,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Navigation Menu" !current.modifier_for_navigation in - let modifier_for_display = + let modifier_for_display = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_display <- l) @@ -488,23 +492,23 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Display Menu" !current.modifier_for_display in - let modifiers_valid = + let modifiers_valid = modifiers ~f:(fun l -> !current.modifiers_valid <- l) "Allowed modifiers" !current.modifiers_valid in - let cmd_editor = + let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo - ~help:"(%s for file name)" + ~help:"(%s for file name)" "External editor" ~f:(fun s -> !current.cmd_editor <- s) ~new_allowed: true (predefined@[if List.mem !current.cmd_editor predefined then "" else !current.cmd_editor]) !current.cmd_editor - in + in let cmd_browse = let predefined = [ Coq_config.browser; @@ -514,40 +518,57 @@ let configure ?(apply=(fun () -> ())) () = "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"; "open -a Safari %s &" ] in - combo - ~help:"(%s for url)" + combo + ~help:"(%s for url)" "Browser" ~f:(fun s -> !current.cmd_browse <- s) ~new_allowed: true (predefined@[if List.mem !current.cmd_browse predefined then "" else !current.cmd_browse]) !current.cmd_browse - in - let doc_url = - string ~f:(fun s -> !current.doc_url <- s) " Manual URL" !current.doc_url in - let library_url = - string ~f:(fun s -> !current.library_url <- s) "Library URL" !current.library_url in - - let automatic_tactics = + in + let doc_url = + let predefined = [ + use_default_doc_url + ] in + combo + "Manual URL" + ~f:(fun s -> !current.doc_url <- s) + ~new_allowed: true + (predefined@[if List.mem !current.doc_url predefined then "" + else !current.doc_url]) + !current.doc_url in + let library_url = + let predefined = [ + Coq_config.wwwstdlib + ] in + combo + "Library URL" + ~f:(fun s -> !current.library_url <- s) + (predefined@[if List.mem !current.library_url predefined then "" + else !current.library_url]) + !current.library_url + in + let automatic_tactics = strings - ~f:(fun l -> !current.automatic_tactics <- l) + ~f:(fun l -> !current.automatic_tactics <- l) ~add:(fun () -> [""]) - "Wizard tactics to try in order" + "Wizard tactics to try in order" !current.automatic_tactics in let contextual_menus_on_goal = - bool - ~f:(fun s -> - !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + bool + ~f:(fun s -> + !current.contextual_menus_on_goal <- s; + !contextual_menus_on_goal s) "Contextual menus on goal" !current.contextual_menus_on_goal - in + in let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; vertical_tabs;opposite_tabs] in - + (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = @@ -557,7 +578,7 @@ let configure ?(apply=(fun () -> ())) () = [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) encodings; - ]); + ]); (* Section("Appearance", config_appearance); @@ -581,6 +602,6 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - match x with + match x with | Return_apply | Return_ok -> save_pref () | Return_cancel -> () -- cgit v1.2.3