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.

1 files changed, 9 insertions, 8 deletions

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