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.

11 files changed, 53 insertions, 70 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9d70d3fc8..6769ce768 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -162,7 +162,6 @@ let load_file ?(maycreate=false) f =
       input_buffer#place_cursor ~where:input_buffer#start_iter;
       Sentence.tag_all input_buffer;
       session.script#clear_undo ();
-      !refresh_editor_hook ();
       Minilib.log "Loading: success";
     end
   with e -> flash_info ("Load failed: "^(Printexc.to_string e))
@@ -248,7 +247,6 @@ module File = struct
 let newfile _ =
   let session = create_session None in
   let index = notebook#append_term session in
-  !refresh_editor_hook ();
   notebook#goto_page index
 
 let load _ =
@@ -812,47 +810,12 @@ let zoom_fit sn =
   let tlen = fst (Pango.Layout.get_pixel_size layout) in
   Pango.Font.set_size (Pango.Font.from_string text_font#get)
     (fsize * space / tlen / Pango.scale * Pango.scale);
-  save_pref ();
-  !refresh_editor_hook ()
+  save_pref ()
 
 end
 
 (** Refresh functions *)
 
-let refresh_editor_prefs () =
-  let wrap_mode = if dynamic_word_wrap#get then `WORD else `NONE in
-  let show_spaces =
-    if show_spaces#get then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *)
-    else 0
-  in
-  let fd = Pango.Font.from_string text_font#get in
-  let iter_session sn =
-    (* Editor settings *)
-    sn.script#set_wrap_mode wrap_mode;
-    sn.script#set_show_line_numbers show_line_number#get;
-    sn.script#set_auto_indent auto_indent#get;
-    sn.script#set_highlight_current_line highlight_current_line#get;
-
-    (* Hack to handle missing binding in lablgtk *)
-    let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int }
-    in
-    Gobject.set conv sn.script#as_widget show_spaces;
-
-    sn.script#set_show_right_margin show_right_margin#get;
-    if show_progress_bar#get then sn.segment#misc#show () else sn.segment#misc#hide ();
-    sn.script#set_insert_spaces_instead_of_tabs spaces_instead_of_tabs#get;
-    sn.script#set_tab_width tab_length#get;
-    sn.script#set_auto_complete auto_complete#get;
-
-    (* Fonts *)
-    sn.script#misc#modify_font fd;
-    sn.proof#misc#modify_font fd;
-    sn.messages#modify_font fd;
-    sn.command#refresh_font ();
-
-  in
-  List.iter iter_session notebook#pages
-
 let refresh_notebook_pos () =
   let pos = match vertical_tabs#get, opposite_tabs#get with
     | false, false -> `TOP
@@ -1060,15 +1023,13 @@ let build_ui () =
           let ft = Pango.Font.from_string text_font#get in
           Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale);
           text_font#set (Pango.Font.to_string ft);
-          save_pref ();
-          !refresh_editor_hook ());
+          save_pref ());
     item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
         ~stock:`ZOOM_OUT ~callback:(fun _ ->
           let ft = Pango.Font.from_string text_font#get in
           Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale);
           text_font#set (Pango.Font.to_string ft);
-          save_pref ();
-          !refresh_editor_hook ());
+          save_pref ());
     item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
         ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit);
     toggle_item "Show Toolbar" ~label:"Show _Toolbar"
@@ -1278,9 +1239,6 @@ let build_ui () =
   let _ = Glib.Timeout.add ~ms:300 ~callback in
 
   (* Initializing hooks *)
-  let refresh_toolbar b =
-    if b then toolbar#misc#show () else toolbar#misc#hide ()
-  in
   let refresh_style style =
     let style = style_manager#style_scheme style in
     let iter_session v = v.script#source_buffer#set_style_scheme style in
@@ -1291,11 +1249,12 @@ let build_ui () =
     let iter_session v = v.script#source_buffer#set_language lang in
     List.iter iter_session notebook#pages
   in
-  refresh_toolbar show_toolbar#get;
-  let _ = show_toolbar#connect#changed refresh_toolbar in
+  let refresh_toolbar b =
+    if b then toolbar#misc#show () else toolbar#misc#hide ()
+  in
+  stick show_toolbar toolbar refresh_toolbar;
   let _ = source_style#connect#changed refresh_style in
   let _ = source_language#connect#changed refresh_language in
-  refresh_editor_hook := refresh_editor_prefs;
 
   (* Color configuration *)
   Tags.Script.incomplete#set_property
@@ -1316,7 +1275,7 @@ let make_file_buffer f =
 let make_scratch_buffer () =
   let session = create_session None in
   let _ = notebook#append_term session in
-  !refresh_editor_hook ()
+  ()
 
 let main files =
   build_ui ();
diff --git a/ide/ide.mllib b/ide/ide.mllib
index e082bd18c..83b314283 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,6 @@ Configwin
 Editable_cells
 Config_parser
 Tags
-Wg_Segment
 Wg_Notebook
 Config_lexer
 Utf8_convert
@@ -21,6 +20,7 @@ Coq
 Coq_lex
 Sentence
 Gtk_parsing
+Wg_Segment
 Wg_ProofView
 Wg_MessageView
 Wg_Detachable
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
 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 351463ea0..d815c01dd 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -91,7 +91,7 @@ val load_pref : unit -> unit
 
 val configure : ?apply:(unit -> unit) -> unit -> unit
 
-(* Hooks *)
-val refresh_editor_hook : (unit -> unit) ref
+val stick : 'a preference ->
+  (#GObj.widget as 'obj) -> ('a -> unit) -> unit
 
 val use_default_doc_url : string
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 1f342bbc4..163bd28b1 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -85,10 +85,11 @@ object(self)
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
     let result = GText.view ~packing:r_bin#add () in
     views <- (frame#coerce, result, combo#entry) :: views;
-    result#misc#modify_font (Pango.Font.from_string text_font#get);
     let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed cb in
     let _ = result#misc#connect#realize (fun () -> cb background_color#get) in
+    let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
+    stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
     let callback () =
@@ -145,10 +146,6 @@ object(self)
 
   method visible =
     frame#visible
-  
-  method refresh_font () =
-    let iter (_,view,_) = view#misc#modify_font (Pango.Font.from_string text_font#get) in
-    List.iter iter views
 
   method private refresh_color clr =
     let clr = Tags.color_of_string clr in
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index c559ebef3..1f0e31988 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -10,7 +10,6 @@ class command_window : string -> Coq.coqtop ->
   object
     method new_query : ?command:string -> ?term:string -> unit -> unit
     method pack_in : (GObj.widget -> unit) -> unit
-    method refresh_font : unit -> unit
     method show : unit
     method hide : unit
     method visible : bool
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 7b7f0fab1..30bb48e3f 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -34,7 +34,6 @@ class type message_view =
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
-    method modify_font : Pango.font_description -> unit
   end
 
 let message_view () : message_view =
@@ -58,6 +57,8 @@ let message_view () : message_view =
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed cb in
   let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+  stick text_font view cb;
   object (self)
     inherit GObj.widget box#as_widget
 
@@ -87,6 +88,4 @@ let message_view () : message_view =
 
     method buffer = text_buffer
 
-    method modify_font fd = view#misc#modify_font fd
-
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 4dcd7306b..457ece090 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -24,7 +24,6 @@ class type message_view =
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
-    method modify_font : Pango.font_description -> unit
   end
 
 val message_view : unit -> message_view
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index e3a741394..6402789ec 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -197,6 +197,9 @@ let proof_view () =
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed cb in
   let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+  stick text_font view cb;
+
   object
     inherit GObj.widget view#as_widget
     val mutable goals = None
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 3b3d9db4b..14cbf92eb 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -462,6 +462,29 @@ object (self)
     let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed cb in
     let _ = self#misc#connect#realize (fun () -> cb background_color#get) in
+
+    let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in
+    stick dynamic_word_wrap self cb;
+    stick show_line_number self self#set_show_line_numbers;
+    stick auto_indent self self#set_auto_indent;
+    stick highlight_current_line self self#set_highlight_current_line;
+
+    (* Hack to handle missing binding in lablgtk *)
+    let cb b =
+      let flag = if b then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) else 0 in
+      let conv = Gobject.({ name = "draw-spaces"; conv = Data.int }) in
+      Gobject.set conv self#as_widget flag
+    in
+    stick show_spaces self cb;
+
+    stick show_right_margin self self#set_show_right_margin;
+    stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs;
+    stick tab_length self self#set_tab_width;
+    stick auto_complete self self#set_auto_complete;
+
+    let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in
+    stick text_font self cb;
+
     ()
 
 end
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 25a031d6e..2ee288454 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Preferences
 
 type color = GDraw.color
 
@@ -122,6 +123,8 @@ object (self)
       true
     in
     let _ = eventbox#event#connect#button_press clicked_cb in
+    let cb show = if show then self#misc#show () else self#misc#hide () in
+    stick show_progress_bar self cb;
     (** Initial pixmap *)
     draw#set_pixmap pixmap