From c53f2f75375dfffd2f258c76f5b722d37ab0daf9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 26 Aug 2015 00:47:26 +0200 Subject: Switching to an event-based mechanism for CoqIDE preferences. There is no remaining hook in the preferences. In particular, the refresh_editor_hook is gone. --- ide/preferences.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index 9432cdb22..8520cce0d 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -61,6 +61,13 @@ object (self) 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 = @@ -181,8 +188,6 @@ let loaded_accel_file = (** Hooks *) -let refresh_editor_hook = ref (fun () -> ()) - (** New style preferences *) let cmd_coqtop = @@ -435,11 +440,7 @@ let configure ?(apply=(fun () -> ())) () = box (fun () -> let fd = w#font_name in - text_font#set 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 @@ -504,7 +505,7 @@ let configure ?(apply=(fun () -> ())) () = 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 () = !refresh_editor_hook () in + let callback () = () in custom ~label box callback true in -- cgit v1.2.3