Replacing old-style preferences in CoqIDE.

There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.

9 files changed, 160 insertions, 217 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index b178ba4ae..2cffdf816 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -130,8 +130,6 @@ end = struct
 end
 open SentenceId
 
-let prefs = Preferences.current
-
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 46d99913e..9d70d3fc8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -44,8 +44,6 @@ open Session
 
 (** {2 Some static elements } *)
 
-let prefs = Preferences.current
-
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
 let custom_project_files = ref []
@@ -89,7 +87,7 @@ let make_coqtop_args = function
     let get_args f = Project_file.args_from_project f
       !custom_project_files project_file_name#get
     in
-    match prefs.read_project with
+    match read_project#get with
       |Ignore_args -> "", !sup_args
       |Append_args ->
          let fname, args = get_args the_file in fname, args @ !sup_args
@@ -421,7 +419,7 @@ let editor sn =
     |Some f ->
       File.save ();
       let f = Filename.quote f in
-      let cmd = Util.subst_command_placeholder prefs.cmd_editor f in
+      let cmd = Util.subst_command_placeholder cmd_editor#get f in
       run_command ignore (fun _ -> sn.fileops#revert) cmd
 
 let editor = cb_on_current_term editor
@@ -809,10 +807,10 @@ let zoom_fit sn =
   let cols = script#right_margin_position in
   let pango_ctx = script#misc#pango_context in
   let layout = pango_ctx#create_layout in
-  let fsize = Pango.Font.get_size current.text_font in
+  let fsize = Pango.Font.get_size (Pango.Font.from_string text_font#get) in
   Pango.Layout.set_text layout (String.make cols 'X');
   let tlen = fst (Pango.Layout.get_pixel_size layout) in
-  Pango.Font.set_size current.text_font
+  Pango.Font.set_size (Pango.Font.from_string text_font#get)
     (fsize * space / tlen / Pango.scale * Pango.scale);
   save_pref ();
   !refresh_editor_hook ()
@@ -827,7 +825,7 @@ let refresh_editor_prefs () =
     if show_spaces#get then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *)
     else 0
   in
-  let fd = prefs.text_font in
+  let fd = Pango.Font.from_string text_font#get in
   let iter_session sn =
     (* Editor settings *)
     sn.script#set_wrap_mode wrap_mode;
@@ -1059,14 +1057,16 @@ let build_ui () =
       ~callback:(fun _ -> notebook#next_page ());
     item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus")
         ~stock:`ZOOM_IN ~callback:(fun _ ->
-          Pango.Font.set_size current.text_font
-            (Pango.Font.get_size current.text_font + Pango.scale);
+          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 ());
     item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
         ~stock:`ZOOM_OUT ~callback:(fun _ ->
-          Pango.Font.set_size current.text_font
-            (Pango.Font.get_size current.text_font - Pango.scale);
+          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 ());
     item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
@@ -1112,7 +1112,7 @@ let build_ui () =
     item "Try Tactics" ~label:"_Try Tactics";
     item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO
       ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar")
-      ~callback:(tactic_wizard_callback prefs.automatic_tactics);
+      ~callback:(tactic_wizard_callback automatic_tactics#get);
     tacitem "auto" "a";
     tacitem "auto with *" "asterisk";
     tacitem "eauto" "e";
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index b8e1861ef..eccd61d0d 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -8,8 +8,6 @@
 
 open Ideutils
 
-let prefs = Preferences.current
-
 let revert_timer = mktimer ()
 let autosave_timer = mktimer ()
 
@@ -120,9 +118,9 @@ object(self)
       | None -> None
       | Some f ->
         let dir = Filename.dirname f in
-        let base = (fst prefs.Preferences.auto_save_name) ^
+        let base = (fst Preferences.auto_save_name#get) ^
           (Filename.basename f) ^
-          (snd prefs.Preferences.auto_save_name)
+          (snd Preferences.auto_save_name#get)
         in Some (Filename.concat dir base)
 
   method private need_auto_save =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 3c5a551c1..053bba805 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -74,7 +74,7 @@ let do_convert s =
   in
   let s =
     if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s)
-    else match current.encoding with
+    else match encoding#get with
       |Preferences.Eutf8 | Preferences.Elocale -> from_loc ()
       |Emanual enc -> try from_manual enc with _ -> from_loc ()
   in
@@ -90,7 +90,7 @@ Please choose a correct encoding in the preference panel.*)";;
 
 let try_export file_name s =
   let s =
-    try match current.encoding with
+    try match encoding#get with
       |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s
       |Elocale ->
 	let is_unicode,char_set = Glib.Convert.get_charset () in
@@ -364,7 +364,7 @@ let run_command display finally cmd =
 (** Web browsing *)
 
 let browse prerr url =
-  let com = Util.subst_command_placeholder current.cmd_browse url in
+  let com = Util.subst_command_placeholder cmd_browse#get url in
   let finally = function
     | Unix.WEXITED 127 ->
       prerr
@@ -375,13 +375,13 @@ let browse prerr url =
   run_command (fun _ -> ()) finally com
 
 let doc_url () =
-  if current.doc_url = use_default_doc_url || current.doc_url = ""
+  if doc_url#get = use_default_doc_url || doc_url#get = ""
   then
     let addr = List.fold_left Filename.concat (Coq_config.docdir)
       ["html";"refman";"index.html"]
     in
     if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
-  else current.doc_url
+  else doc_url#get
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 74ca6ca83..9432cdb22 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -63,6 +63,51 @@ end
 
 (** Useful marshallers *)
 
+let mod_to_str m =
+  match m with
+    | `MOD1 -> "<Alt>"
+    | `MOD2 -> "<Mod2>"
+    | `MOD3 -> "<Mod3>"
+    | `MOD4 -> "<Mod4>"
+    | `MOD5 -> "<Mod5>"
+    | `CONTROL -> "<Control>"
+    | `SHIFT -> "<Shift>"
+    | `HYPER -> "<Hyper>"
+    | `META -> "<Meta>"
+    | `RELEASE -> ""
+    | `SUPER -> "<Super>"
+    |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
+
+let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
+
+let str_to_mod_list s = snd (GtkData.AccelGroup.parse s)
+
+type project_behavior = Ignore_args | Append_args | Subst_args
+
+let string_of_project_behavior = function
+  |Ignore_args -> "ignored"
+  |Append_args -> "appended to arguments"
+  |Subst_args -> "taken instead of arguments"
+
+let project_behavior_of_string s =
+  if s = "taken instead of arguments" then Subst_args
+  else if s = "appended to arguments" then Append_args
+  else Ignore_args
+
+type inputenc = Elocale | Eutf8 | Emanual of string
+
+let string_of_inputenc = function
+  |Elocale -> "LOCALE"
+  |Eutf8 -> "UTF-8"
+  |Emanual s -> s
+
+let inputenc_of_string s =
+      (if s = "UTF-8" then Eutf8
+       else if s = "LOCALE" then Elocale
+       else Emanual s)
+
+let use_default_doc_url = "(automatic)"
+
 module Repr =
 struct
 
@@ -72,6 +117,18 @@ object
   method into = function [s] -> Some s | _ -> None
 end
 
+let string_pair : (string * string) repr =
+object
+  method from (s1, s2) = [s1; s2]
+  method into = function [s1; s2] -> Some (s1, s2) | _ -> None
+end
+
+let string_list : string list repr =
+object
+  method from s = s
+  method into s = Some s
+end
+
 let bool : bool repr =
 object
   method from s = [string_of_bool s]
@@ -98,6 +155,14 @@ object
   | _ -> None
 end
 
+let custom (from : 'a -> string) (into : string -> 'a) : 'a repr =
+object
+  method from x = try [from x] with _ -> []
+  method into = function
+  | [s] -> (try Some (into s) with _ -> None)
+  | _ -> None
+end
+
 end
 
 let get_config_file name =
@@ -114,50 +179,6 @@ let loaded_accel_file =
   try get_config_file "coqide.keys"
   with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"
 
-let mod_to_str m =
-  match m with
-    | `MOD1 -> "<Alt>"
-    | `MOD2 -> "<Mod2>"
-    | `MOD3 -> "<Mod3>"
-    | `MOD4 -> "<Mod4>"
-    | `MOD5 -> "<Mod5>"
-    | `CONTROL -> "<Control>"
-    | `SHIFT -> "<Shift>"
-    | `HYPER -> "<Hyper>"
-    | `META -> "<Meta>"
-    | `RELEASE -> ""
-    | `SUPER -> "<Super>"
-    |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
-
-let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
-
-let str_to_mod_list s = snd (GtkData.AccelGroup.parse s)
-
-type project_behavior = Ignore_args | Append_args | Subst_args
-
-let string_of_project_behavior = function
-  |Ignore_args -> "ignored"
-  |Append_args -> "appended to arguments"
-  |Subst_args -> "taken instead of arguments"
-
-let project_behavior_of_string s =
-  if s = "taken instead of arguments" then Subst_args
-  else if s = "appended to arguments" then Append_args
-  else Ignore_args
-
-type inputenc = Elocale | Eutf8 | Emanual of string
-
-let string_of_inputenc = function
-  |Elocale -> "LOCALE"
-  |Eutf8 -> "UTF-8"
-  |Emanual s -> s
-
-let inputenc_of_string s =
-      (if s = "UTF-8" then Eutf8
-       else if s = "LOCALE" then Elocale
-       else Emanual s)
-
-
 (** Hooks *)
 
 let refresh_editor_hook = ref (fun () -> ())
@@ -197,10 +218,12 @@ let auto_save =
 let auto_save_delay =
   new preference ~name:["auto_save_delay"] ~init:10000 ~repr:Repr.(int)
 
-(* let auto_save_name =
-  new preference ~name:["auto_save_name"] ~init: ~repr:Repr.() *)
-(* let read_project =
-  new preference ~name:["read_project"] ~init: ~repr:Repr.() *)
+let auto_save_name =
+  new preference ~name:["auto_save_name"] ~init:("#","#") ~repr:Repr.(string_pair)
+
+let read_project =
+  let repr = Repr.custom string_of_project_behavior project_behavior_of_string in
+  new preference ~name:["read_project"] ~init:Append_args ~repr
 
 let project_file_name =
   new preference ~name:["project_file_name"] ~init:"_CoqProject" ~repr:Repr.(string)
@@ -208,10 +231,14 @@ let project_file_name =
 let project_path =
   new preference ~name:["project_path"] ~init:None ~repr:Repr.(option string)
 
-(* let encoding =
-  new preference ~name:["encoding"] ~init: ~repr:Repr.() *)
-(* let automatic_tactics =
-  new preference ~name:["automatic_tactics"] ~init: ~repr:Repr.() *)
+let encoding =
+  let repr = Repr.custom string_of_inputenc inputenc_of_string in
+  let init = if Sys.os_type = "Win32" then Eutf8 else Elocale in
+  new preference ~name:["encoding"] ~init ~repr
+
+let automatic_tactics =
+  let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in
+  new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list)
 
 let cmd_print =
   new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string)
@@ -231,14 +258,35 @@ let modifier_for_display =
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
 
-(* let cmd_browse =
-  new preference ~name:["cmd_browse"] ~init: ~repr:Repr.() *)
-(* let cmd_editor =
-  new preference ~name:["cmd_editor"] ~init: ~repr:Repr.() *)
-(* let text_font =
-  new preference ~name:["text_font"] ~init: ~repr:Repr.() *)
-(* let doc_url =
-  new preference ~name:["doc_url"] ~init: ~repr:Repr.() *)
+let cmd_browse =
+  new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string)
+
+let cmd_editor =
+  let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in
+  new preference ~name:["cmd_editor"] ~init ~repr:Repr.(string)
+
+let text_font =
+  let init = match Coq_config.gtk_platform with
+  | `QUARTZ -> "Arial Unicode MS 11"
+  | _ -> "Monospace 10"
+  in
+  new preference ~name:["text_font"] ~init ~repr:Repr.(string)
+
+let doc_url =
+object
+  inherit [string] preference
+    ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
+    as super
+
+  method set v =
+    if not (Flags.is_standard_doc_url v) &&
+      v <> use_default_doc_url &&
+      (* Extra hack to support links to last released doc version *)
+      v <> Coq_config.wwwcoq ^ "doc" &&
+      v <> Coq_config.wwwcoq ^ "doc/"
+    then super#set v
+
+end
 
 let library_url =
   new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)
@@ -333,73 +381,15 @@ let nanoPG =
 
 (** Old style preferences *)
 
-type pref =
-    {
-
-      mutable auto_save_name : string * string;
-
-      mutable read_project : project_behavior;
-
-      mutable encoding : inputenc;
-
-      mutable automatic_tactics : string list;
-
-      mutable cmd_browse : string;
-      mutable cmd_editor : string;
-
-      mutable text_font : Pango.font_description;
-
-      mutable doc_url : string;
-
-}
-
-let use_default_doc_url = "(automatic)"
-
-let current = {
-
-    auto_save_name = "#","#";
-
-    read_project = Append_args;
-
-    encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale;
-
-    automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
-			 "auto with *"; "intuition" ];
-
-    cmd_browse = Flags.browser_cmd_fmt;
-    cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s";
-
-(*    text_font = Pango.Font.from_string "sans 12";*)
-    text_font = Pango.Font.from_string (match Coq_config.gtk_platform with
-					  |`QUARTZ -> "Arial Unicode MS 11"
-					  |_ -> "Monospace 10");
-
-    doc_url = Coq_config.wwwrefman;
-  }
-
 let save_pref () =
   if not (Sys.file_exists (Minilib.coqide_config_home ()))
   then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
-  let p = current in
   let add = Util.String.Map.add in
   let (++) x f = f x in
   let fold key obj accu = add key (obj.get ()) accu in
  
     (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++
-    add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++
-
-    add "project_options" [string_of_project_behavior p.read_project] ++
-
-    add "encoding" [string_of_inputenc p.encoding] ++
-
-    add "automatic_tactics" p.automatic_tactics ++
-    add "cmd_browse" [p.cmd_browse] ++
-    add "cmd_editor" [p.cmd_editor] ++
-
-    add "text_font" [Pango.Font.to_string p.text_font] ++
-
-    add "doc_url" [p.doc_url] ++
     Config_lexer.print_file pref_file
 
 let load_pref () =
@@ -410,33 +400,7 @@ let load_pref () =
       try (Util.String.Map.find name !preferences).set v
       with _ -> ()
     in
-    let () = Util.String.Map.iter iter m in
-    let np = current in
-    let set k f = try let v = Util.String.Map.find k m in f v with _ -> () in
-    let set_hd k f = set k (fun v -> f (List.hd v)) in
-    let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in
-    let set_command_with_pair_compat k f =
-      set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
-    in
-    set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2));
-    set_hd "encoding" (fun v -> np.encoding <- (inputenc_of_string v));
-    set_hd "project_options"
-      (fun v -> np.read_project <- (project_behavior_of_string v));
-    set "automatic_tactics"
-      (fun v -> np.automatic_tactics <- v);
-    set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v);
-    set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
-    set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
-    set_hd "doc_url" (fun v ->
-      if not (Flags.is_standard_doc_url v) &&
-        v <> use_default_doc_url &&
-	(* Extra hack to support links to last released doc version *)
-        v <> Coq_config.wwwcoq ^ "doc" &&
-	v <> Coq_config.wwwcoq ^ "doc/"
-      then
-	(* ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*)
-      np.doc_url <- v);
-    ()
+    Util.String.Map.iter iter m
 
 let pstring name p = string ~f:p#set name p#get
 let pbool name p = bool ~f:p#set name p#get
@@ -465,14 +429,13 @@ let configure ?(apply=(fun () -> ())) () =
       "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
     box#pack ~expand:true w#coerce;
     ignore (w#misc#connect#realize
-	      ~callback:(fun () -> w#set_font_name
-			   (Pango.Font.to_string current.text_font)));
+	      ~callback:(fun () -> w#set_font_name text_font#get));
     custom
       ~label:"Fonts for text"
       box
       (fun () ->
 	 let fd =  w#font_name in
-	 current.text_font <- (Pango.Font.from_string fd) ;
+	 text_font#set fd ;
 (*
 	 Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string current.text_font);
 *)
@@ -601,13 +564,13 @@ let configure ?(apply=(fun () -> ())) () =
   let encodings =
     combo
       "File charset encoding "
-      ~f:(fun s -> current.encoding <- (inputenc_of_string s))
+      ~f:(fun s -> encoding#set (inputenc_of_string s))
       ~new_allowed: true
-      ("UTF-8"::"LOCALE":: match current.encoding with
+      ("UTF-8"::"LOCALE":: match encoding#get with
 	|Emanual s -> [s]
 	|_ -> []
       )
-      (string_of_inputenc current.encoding)
+      (string_of_inputenc encoding#get)
   in
 
   let source_style =
@@ -628,12 +591,12 @@ let configure ?(apply=(fun () -> ())) () =
   let read_project =
     combo
       "Project file options are"
-      ~f:(fun s -> current.read_project <- project_behavior_of_string s)
+      ~f:(fun s -> read_project#set (project_behavior_of_string s))
       ~editable:false
       [string_of_project_behavior Subst_args;
        string_of_project_behavior Append_args;
        string_of_project_behavior Ignore_args]
-      (string_of_project_behavior current.read_project)
+      (string_of_project_behavior read_project#get)
   in
   let project_file_name = pstring "Default name for project file" project_file_name in
   let modifier_for_tactics =
@@ -656,11 +619,11 @@ let configure ?(apply=(fun () -> ())) () =
     combo
       ~help:"(%s for file name)"
       "External editor"
-      ~f:(fun s -> current.cmd_editor <- s)
+      ~f:cmd_editor#set
       ~new_allowed: true
-      (predefined@[if List.mem current.cmd_editor predefined then ""
-                   else current.cmd_editor])
-      current.cmd_editor
+      (predefined@[if List.mem cmd_editor#get predefined then ""
+                   else cmd_editor#get])
+      cmd_editor#get
   in
   let cmd_browse =
     let predefined = [
@@ -673,11 +636,11 @@ let configure ?(apply=(fun () -> ())) () =
     combo
       ~help:"(%s for url)"
       "Browser"
-      ~f:(fun s -> current.cmd_browse <- s)
+      ~f:cmd_browse#set
       ~new_allowed: true
-      (predefined@[if List.mem current.cmd_browse predefined then ""
-                   else current.cmd_browse])
-      current.cmd_browse
+      (predefined@[if List.mem cmd_browse#get predefined then ""
+                   else cmd_browse#get])
+      cmd_browse#get
   in
   let doc_url =
     let predefined = [
@@ -687,11 +650,11 @@ let configure ?(apply=(fun () -> ())) () =
     ] in
     combo
       "Manual URL"
-      ~f:(fun s -> current.doc_url <- s)
+      ~f:doc_url#set
       ~new_allowed: true
-      (predefined@[if List.mem current.doc_url predefined then ""
-                   else current.doc_url])
-      current.doc_url in
+      (predefined@[if List.mem doc_url#get predefined then ""
+                   else doc_url#get])
+      doc_url#get in
   let library_url =
     let predefined = [
       "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]);
@@ -707,10 +670,10 @@ let configure ?(apply=(fun () -> ())) () =
   in
   let automatic_tactics =
     strings
-      ~f:(fun l -> current.automatic_tactics <- l)
+      ~f:automatic_tactics#set
       ~add:(fun () -> ["<edit me>"])
       "Wizard tactics to try in order"
-      current.automatic_tactics
+      automatic_tactics#get
 
   in
 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 48c2a6410..351463ea0 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -44,22 +44,22 @@ val global_auto_revert : bool preference
 val global_auto_revert_delay : int preference
 val auto_save : bool preference
 val auto_save_delay : int preference
-(* val auto_save_name : string * string preference *)
-(* val read_project : project_behavior preference *)
+val auto_save_name : (string * string) preference
+val read_project : project_behavior preference
 val project_file_name : string preference
 val project_path : string option preference
-(* val encoding : inputenc preference *)
-(* val automatic_tactics : string list preference *)
+val encoding : inputenc preference
+val automatic_tactics : string list preference
 val cmd_print : string preference
 val modifier_for_navigation : string preference
 val modifier_for_templates : string preference
 val modifier_for_tactics : string preference
 val modifier_for_display : string preference
 val modifiers_valid : string preference
-(* val cmd_browse : string preference *)
-(* val cmd_editor : string preference *)
-(* val text_font : Pango.font_description preference *)
-(* val doc_url : string preference *)
+val cmd_browse : string preference
+val cmd_editor : string preference
+val text_font : string preference
+val doc_url : string preference
 val library_url : string preference
 val show_toolbar : bool preference
 val contextual_menus_on_goal : bool preference
@@ -86,23 +86,9 @@ val tab_length : int preference
 val highlight_current_line : bool preference
 val nanoPG : bool preference
 
-type pref =
-    {
-      mutable auto_save_name : string * string;
-      mutable read_project : project_behavior;
-      mutable encoding : inputenc;
-      mutable automatic_tactics : string list;
-      mutable cmd_browse : string;
-      mutable cmd_editor : string;
-      mutable text_font : Pango.font_description;
-      mutable doc_url : string;
-    }
-
 val save_pref : unit -> unit
 val load_pref : unit -> unit
 
-val current : pref
-
 val configure : ?apply:(unit -> unit) -> unit -> unit
 
 (* Hooks *)
diff --git a/ide/session.ml b/ide/session.ml
index ceeb0abca..e4cc17742 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -8,8 +8,6 @@
 
 open Preferences
 
-let prefs = Preferences.current
-
 (** A session is a script buffer + proof + messages,
     interacting with a coqtop, and a few other elements around *)
 
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index bfd37ea0e..1f342bbc4 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -85,7 +85,7 @@ 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 current.text_font;
+    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
@@ -147,7 +147,7 @@ object(self)
     frame#visible
   
   method refresh_font () =
-    let iter (_,view,_) = view#misc#modify_font current.text_font in
+    let iter (_,view,_) = view#misc#modify_font (Pango.Font.from_string text_font#get) in
     List.iter iter views
 
   method private refresh_color clr =
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 3f5ae4bd5..7d77679ce 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -258,7 +258,7 @@ object (self)
 
   method private refresh_style () =
     let (renderer, _) = renderer in
-    let font = Preferences.current.Preferences.text_font in
+    let font = Pango.Font.from_string Preferences.text_font#get in
     renderer#set_properties [`FONT_DESC font; `XPAD 10]
 
   method private coordinates pos =