diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 42 |
1 files changed, 13 insertions, 29 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 90862d06..f7cc27a5 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -711,61 +711,38 @@ let configure ?(apply=(fun () -> ())) () = ~f:(fun s -> current.project_file_name <- s) current.project_file_name in - let update_modifiers prefix mds = - 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 let help_string = "restart to apply" in let the_valid_mod = str_to_mod_list current.modifiers_valid in let modifier_for_tactics = - let cb l = - current.modifier_for_tactics <- mod_list_to_str l; - update_modifiers "<Actions>/Tactics/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~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) in let modifier_for_templates = - let cb l = - current.modifier_for_templates <- mod_list_to_str l; - update_modifiers "<Actions>/Templates/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~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) in let modifier_for_navigation = - let cb l = - current.modifier_for_navigation <- mod_list_to_str l; - update_modifiers "<Actions>/Navigation/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~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) in let modifier_for_display = - let cb l = - current.modifier_for_display <- mod_list_to_str l; - update_modifiers "<Actions>/View/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~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) @@ -777,6 +754,13 @@ let configure ?(apply=(fun () -> ())) () = "Allowed modifiers" the_valid_mod in + let modifier_notice = + let b = GPack.hbox () in + let _lbl = + GMisc.label ~markup:"You need to <b>restart CoqIDE</b> after changing these settings" + ~packing:b#add () in + custom b (fun () -> ()) true + in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo @@ -878,7 +862,7 @@ 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_for_templates; modifier_for_display; modifier_for_navigation; modifier_notice]); Section("Misc", Some `ADD, misc)] in |