Taking advantage of the new type of preferences.

We use uniform functions instead of code duplication.
Likewise, we disentangle the hook mechanisms by using
callbacks connected to preferences instead.

Only the easy hook bits were removed. The most awing one,
the editor refreshing hook, is still alive.

3 files changed, 61 insertions, 149 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index d90e9153c..e8bdf5e0e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1087,52 +1087,35 @@ let build_ui () =
         ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit);
     toggle_item "Show Toolbar" ~label:"Show _Toolbar"
       ~active:(show_toolbar#get)
-      ~callback:(fun _ ->
-        show_toolbar#set (not show_toolbar#get);
-        !refresh_toolbar_hook ());
+      ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get));
     item "Query Pane" ~label:"_Query Pane"
       ~accel:"F1"
       ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;
 
-  menu navigation_menu [
-    item "Navigation" ~label:"_Navigation";
-    item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one
-      ~tooltip:"Forward one command"
-      ~accel:(modifier_for_navigation#get ^"Down");
-    item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one
-      ~tooltip:"Backward one command"
-      ~accel:(modifier_for_navigation#get ^"Up");
-    item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto
-      ~tooltip:"Go to cursor"
-      ~accel:(modifier_for_navigation#get ^"Right");
-    item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart
-      ~tooltip:"Restart coq"
-      ~accel:(modifier_for_navigation#get ^"Home");
-    item "End" ~label:"_End" ~stock:`GOTO_BOTTOM  ~callback:Nav.goto_end
-      ~tooltip:"Go to end"
-      ~accel:(modifier_for_navigation#get ^"End");
-    item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt
-      ~tooltip:"Interrupt computations"
-      ~accel:(modifier_for_navigation#get ^"Break");
-(* wait for this available in GtkSourceView !
-      item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
-	~callback:(fun _ -> let sess = notebook#current_term in
-		     toggle_proof_visibility sess.buffer
-		       sess.analyzed_view#get_insert) ~tooltip:"Hide proof"
-	~accel:(prefs.modifier_for_navigation^"h");*)
-    item "Previous" ~label:"_Previous" ~stock:`GO_BACK
-      ~callback:Nav.previous_occ
-      ~tooltip:"Previous occurence"
-      ~accel:(modifier_for_navigation#get ^"less");
-    item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
-      ~tooltip:"Next occurence"
-      ~accel:(modifier_for_navigation#get ^"greater");
-    item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
-      ~tooltip:"Fully check the document" 
-      ~accel:(modifier_for_navigation#get ^"f"); 
-  ];
+  let navitem (text, label, stock, callback, tooltip, accel) =
+    let accel = modifier_for_navigation#get ^ accel in
+    item text ~label ~stock ~callback ~tooltip ~accel
+  in
+  menu navigation_menu begin
+  [
+    (fun e -> item "Navigation" ~label:"_Navigation" e);
+  ] @ List.map navitem [
+    ("Forward", "_Forward", `GO_DOWN, Nav.forward_one, "Forward one command", "Down");
+    ("Backward", "_Backward", `GO_UP, Nav.backward_one, "Backward one command", "Up");
+    ("Go to", "_Go to", `JUMP_TO, Nav.goto, "Go to cursor", "Right");
+    ("Start", "_Start", `GOTO_TOP, Nav.restart, "Restart coq", "Home");
+    ("End", "_End", `GOTO_BOTTOM, Nav.goto_end, "Go to end", "End");
+    ("Interrupt", "_Interrupt", `STOP, Nav.interrupt, "Interrupt computations", "Break");
+    (* wait for this available in GtkSourceView !
+    ("Hide", "_Hide", `MISSING_IMAGE,
+        ~callback:(fun _ -> let sess = notebook#current_term in
+          toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *)
+    ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less");
+    ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater");
+    ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
+  ] end;
 
   let tacitem s sc =
     item s ~label:("_"^s)
@@ -1309,31 +1292,24 @@ let build_ui () =
   let _ = Glib.Timeout.add ~ms:300 ~callback in
 
   (* Initializing hooks *)
-  let refresh_toolbar () =
-    if show_toolbar#get
-    then toolbar#misc#show ()
-    else toolbar#misc#hide ()
+  let refresh_toolbar b =
+    if b then toolbar#misc#show () else toolbar#misc#hide ()
   in
-  let refresh_style () =
-    let style =  style_manager#style_scheme source_style#get 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
     List.iter iter_session notebook#pages
   in
-  let refresh_language () =
-    let lang =  lang_manager#language source_language#get in
+  let refresh_language lang =
+    let lang = lang_manager#language lang in
     let iter_session v = v.script#source_buffer#set_language lang in
     List.iter iter_session notebook#pages
   in
-  let resize_window () =
-    w#resize ~width:window_width#get ~height:window_height#get
-  in
-  refresh_toolbar ();
-  refresh_toolbar_hook := refresh_toolbar;
-  refresh_style_hook := refresh_style;
-  refresh_language_hook := refresh_language;
+  refresh_toolbar show_toolbar#get;
+  let _ = show_toolbar#connect#changed refresh_toolbar in
+  let _ = source_style#connect#changed refresh_style in
+  let _ = source_language#connect#changed refresh_language in
   refresh_editor_hook := refresh_editor_prefs;
-  resize_window_hook := resize_window;
-  refresh_tabs_hook := refresh_notebook_pos;
 
   (* Color configuration *)
   Tags.Script.incomplete#set_property
diff --git a/ide/preferences.ml b/ide/preferences.ml
index f8149b4f6..ceae6d1be 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -158,12 +158,7 @@ let inputenc_of_string s =
 
 (** Hooks *)
 
-let refresh_style_hook = ref (fun () -> ())
-let refresh_language_hook = ref (fun () -> ())
 let refresh_editor_hook = ref (fun () -> ())
-let refresh_toolbar_hook = ref (fun () -> ())
-let resize_window_hook = ref (fun () -> ())
-let refresh_tabs_hook = ref (fun () -> ())
 
 (** New style preferences *)
 
@@ -427,6 +422,12 @@ let load_pref () =
 
 let pstring name p = string ~f:p#set name p#get
 let pbool name p = bool ~f:p#set name p#get
+let pmodifiers ?(all = false) name p = modifiers
+  ?allow:(if all then None else Some (str_to_mod_list modifiers_valid#get))
+  ~f:(fun l -> p#set (mod_list_to_str l))
+  ~help:"restart to apply"
+  name
+  (str_to_mod_list p#get)
 
 let configure ?(apply=(fun () -> ())) () =
   let cmd_coqtop =
@@ -544,46 +545,22 @@ let configure ?(apply=(fun () -> ())) () =
   let config_editor =
     let label = "Editor configuration" in
     let box = GPack.vbox () in
-    let gen_button text active =
-      GButton.check_button ~label:text ~active ~packing:box#pack () in
-    let wrap = gen_button "Dynamic word wrap" dynamic_word_wrap#get in
-    let line = gen_button "Show line number" show_line_number#get in
-    let b_auto_indent = gen_button "Auto indentation" auto_indent#get in
-    let b_auto_complete = gen_button "Auto completion" auto_complete#get in
-    let b_show_spaces = gen_button "Show spaces" show_spaces#get in
-    let b_show_right_margin = gen_button "Show right margin" show_right_margin#get in
-    let b_show_progress_bar = gen_button "Show progress bar" show_progress_bar#get in
-    let b_spaces_instead_of_tabs =
-      gen_button "Insert spaces instead of tabs"
-      spaces_instead_of_tabs#get
-    in
-    let b_highlight_current_line =
-      gen_button "Highlight current line"
-      highlight_current_line#get
-    in
-    let b_nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" nanoPG#get in
-(*     let lbox = GPack.hbox ~packing:box#pack () in *)
-(*     let _ = GMisc.label ~text:"Tab width" *)
-(*         ~xalign:0. *)
-(*         ~packing:(lbox#pack ~expand:true) () *)
-(*     in *)
-(*     let tab_width = GEdit.spin_button *)
-(*       ~digits:0 ~packing:lbox#pack () *)
-(*     in *)
-    let callback () =
-      dynamic_word_wrap#set wrap#active;
-      show_line_number#set line#active;
-      auto_indent#set b_auto_indent#active;
-      show_spaces#set b_show_spaces#active;
-      show_right_margin#set b_show_right_margin#active;
-      show_progress_bar#set b_show_progress_bar#active;
-      spaces_instead_of_tabs#set b_spaces_instead_of_tabs#active;
-      highlight_current_line#set b_highlight_current_line#active;
-      nanoPG#set b_nanoPG#active;
-      auto_complete#set b_auto_complete#active;
-(*       tab_length#set tab_width#value_as_int; *)
-      !refresh_editor_hook ()
+    let button text (pref : bool preference) =
+      let active = pref#get in
+      let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
+      ignore (but#connect#toggled (fun () -> pref#set but#active))
     in
+    let () = button "Dynamic word wrap" dynamic_word_wrap in
+    let () = button "Show line number" show_line_number in
+    let () = button "Auto indentation" auto_indent in
+    let () = button "Auto completion" auto_complete in
+    let () = button "Show spaces" show_spaces in
+    let () = button "Show right margin" show_right_margin in
+    let () = button "Show progress bar" show_progress_bar in
+    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
     custom ~label box callback true
   in
 
@@ -653,22 +630,14 @@ let configure ?(apply=(fun () -> ())) () =
   in
 
   let source_style =
-    let f s =
-      source_style#set s;
-      !refresh_style_hook ()
-    in
     combo "Highlighting style:"
-      ~f ~new_allowed:false
+      ~f:source_style#set ~new_allowed:false
       style_manager#style_scheme_ids source_style#get
   in
 
   let source_language =
-    let f s =
-      source_language#set s;
-      !refresh_language_hook ()
-    in
     combo "Language:"
-      ~f ~new_allowed:false
+      ~f:source_language#set ~new_allowed:false
       (List.filter
         (fun x -> Str.string_match (Str.regexp "^coq") x 0)
         lang_manager#language_ids)
@@ -686,48 +655,20 @@ let configure ?(apply=(fun () -> ())) () =
       (string_of_project_behavior current.read_project)
   in
   let project_file_name = pstring "Default name for project file" project_file_name in
-  let help_string =
-    "restart to apply"
-  in
-  let the_valid_mod = str_to_mod_list modifiers_valid#get in
   let modifier_for_tactics =
-    modifiers
-      ~allow:the_valid_mod
-      ~f:(fun l -> modifier_for_tactics#set (mod_list_to_str l))
-      ~help:help_string
-      "Modifiers for Tactics Menu"
-      (str_to_mod_list modifier_for_tactics#get)
+    pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics
   in
   let modifier_for_templates =
-    modifiers
-      ~allow:the_valid_mod
-      ~f:(fun l -> modifier_for_templates#set (mod_list_to_str l))
-      ~help:help_string
-      "Modifiers for Templates Menu"
-      (str_to_mod_list modifier_for_templates#get)
+    pmodifiers "Modifiers for Templates Menu" modifier_for_templates
   in
   let modifier_for_navigation =
-    modifiers
-      ~allow:the_valid_mod
-      ~f:(fun l -> modifier_for_navigation#set (mod_list_to_str l))
-      ~help:help_string
-      "Modifiers for Navigation Menu"
-      (str_to_mod_list modifier_for_navigation#get)
+    pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation
   in
   let modifier_for_display =
-    modifiers
-      ~allow:the_valid_mod
-      ~f:(fun l -> modifier_for_display#set (mod_list_to_str l))
-      ~help:help_string
-      "Modifiers for View Menu"
-      (str_to_mod_list modifier_for_display#get)
+    pmodifiers "Modifiers for View Menu" modifier_for_display
   in
   let modifiers_valid =
-    modifiers
-      ~f:(fun l ->
-	modifiers_valid#set (mod_list_to_str l))
-      "Allowed modifiers"
-      the_valid_mod
+    pmodifiers ~all:true "Allowed modifiers" modifiers_valid
   in
   let cmd_editor =
     let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 0a83e609b..1da8b3157 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -105,10 +105,5 @@ val configure : ?apply:(unit -> unit) -> unit -> unit
 
 (* Hooks *)
 val refresh_editor_hook : (unit -> unit) ref
-val refresh_style_hook : (unit -> unit) ref
-val refresh_language_hook : (unit -> unit) ref
-val refresh_toolbar_hook : (unit -> unit) ref
-val resize_window_hook : (unit -> unit) ref
-val refresh_tabs_hook : (unit -> unit) ref
 
 val use_default_doc_url : string