Turning CoqIDE preferences into new style.

Some old style references remain because all type converters are not
implemented yet.

11 files changed, 347 insertions, 478 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index b7753e6e8..d061df6fd 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -125,7 +125,7 @@ and asks_for_coqtop args =
     ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
   match pb_mes#run () with
     | `YES ->
-      let () = current.cmd_coqtop  <- None in
+      let () = cmd_coqtop#set None in
       let () = custom_coqtop := None in
       let () = pb_mes#destroy () in
       filter_coq_opts args
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c6d314947..7f44ec2aa 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -630,7 +630,7 @@ object(self)
 
   method private process_until_iter iter =
     let until _ start stop =
-      if prefs.Preferences.stop_before then stop#compare iter > 0
+      if Preferences.stop_before#get then stop#compare iter > 0
       else start#compare iter >= 0
     in
     self#process_until until false
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c0e228125..d90e9153c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -87,7 +87,7 @@ let make_coqtop_args = function
   |None -> "", !sup_args
   |Some the_file ->
     let get_args f = Project_file.args_from_project f
-      !custom_project_files prefs.project_file_name
+      !custom_project_files project_file_name#get
     in
     match prefs.read_project with
       |Ignore_args -> "", !sup_args
@@ -319,7 +319,7 @@ let export kind sn =
           | _ -> assert false
       in
       let cmd =
-        local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^
+        local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
       sn.messages#set ("Running: "^cmd);
@@ -334,8 +334,8 @@ let print sn =
     |None -> flash_info "Cannot print: this buffer has no name"
     |Some f_name ->
       let cmd =
-        local_cd f_name ^ prefs.cmd_coqdoc ^ " -ps " ^
-        Filename.quote (Filename.basename f_name) ^ " | " ^ prefs.cmd_print
+        local_cd f_name ^ cmd_coqdoc#get ^ " -ps " ^
+        Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get
       in
       let w = GWindow.window ~title:"Print" ~modal:true
         ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" ()
@@ -378,17 +378,17 @@ end
 
 let reset_revert_timer () =
   FileOps.revert_timer.kill ();
-  if prefs.global_auto_revert then
+  if global_auto_revert#get then
     FileOps.revert_timer.run
-      ~ms:prefs.global_auto_revert_delay
+      ~ms:global_auto_revert_delay#get
       ~callback:(fun () -> File.revert_all (); true)
 
 let reset_autosave_timer () =
   let autosave sn = try sn.fileops#auto_save with _ -> () in
   let autosave_all () = List.iter autosave notebook#pages; true in
   FileOps.autosave_timer.kill ();
-  if prefs.auto_save then
-    FileOps.autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all
+  if auto_save#get then
+    FileOps.autosave_timer.run ~ms:auto_save_delay#get ~callback:autosave_all
 
 (** Export of functions used in [coqide_main] : *)
 
@@ -408,8 +408,8 @@ let coq_makefile sn =
   match sn.fileops#filename with
     |None -> flash_info "Cannot make makefile: this buffer has no name"
     |Some f ->
-      let cmd = local_cd f ^ prefs.cmd_coqmakefile in
-      let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st)
+      let cmd = local_cd f ^ cmd_coqmakefile#get in
+      let finally st = flash_info (cmd_coqmakefile#get ^ pr_exit_status st)
       in
       run_command ignore finally cmd
 
@@ -431,7 +431,7 @@ let compile sn =
   match sn.fileops#filename with
     |None -> flash_info "Active buffer has no name"
     |Some f ->
-      let cmd = prefs.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f))
+      let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f))
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
@@ -467,7 +467,7 @@ let make sn =
     |None -> flash_info "Cannot make: this buffer has no name"
     |Some f ->
       File.saveall ();
-      let cmd = local_cd f ^ prefs.cmd_make ^ " 2>&1" in
+      let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
       sn.messages#set "Compilation output:\n";
       Buffer.reset last_make_buf;
       last_make := "";
@@ -477,7 +477,7 @@ let make sn =
         sn.messages#add s;
         Buffer.add_string last_make_buf s
       in
-      let finally st = flash_info (current.cmd_make ^ pr_exit_status st)
+      let finally st = flash_info (cmd_make#get ^ pr_exit_status st)
       in
       run_command display finally cmd
 
@@ -537,7 +537,7 @@ let update_status sn =
       | None -> ""
       | Some n -> ", proving " ^ n
     in
-    display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name);
+    display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
   Coq.bind (Coq.status ~logger:sn.messages#push false) next
@@ -822,32 +822,31 @@ end
 (** Refresh functions *)
 
 let refresh_editor_prefs () =
-  let wrap_mode = if prefs.dynamic_word_wrap then `WORD else `NONE in
+  let wrap_mode = if dynamic_word_wrap#get then `WORD else `NONE in
   let show_spaces =
-    if prefs.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *)
+    if show_spaces#get then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *)
     else 0
   in
   let fd = prefs.text_font in
-  let clr = Tags.color_of_string prefs.background_color
+  let clr = Tags.color_of_string background_color#get
   in
   let iter_session sn =
     (* Editor settings *)
     sn.script#set_wrap_mode wrap_mode;
-    sn.script#set_show_line_numbers prefs.show_line_number;
-    sn.script#set_auto_indent prefs.auto_indent;
-    sn.script#set_highlight_current_line prefs.highlight_current_line;
+    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 prefs.show_right_margin;
-    if prefs.show_progress_bar then sn.segment#misc#show () else sn.segment#misc#hide ();
-    sn.script#set_insert_spaces_instead_of_tabs
-      prefs.spaces_instead_of_tabs;
-    sn.script#set_tab_width prefs.tab_length;
-    sn.script#set_auto_complete prefs.auto_complete;
+    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;
@@ -856,10 +855,10 @@ let refresh_editor_prefs () =
     sn.command#refresh_font ();
 
     (* Colors *)
-    Tags.set_processing_color (Tags.color_of_string current.processing_color);
-    Tags.set_processed_color (Tags.color_of_string current.processed_color);
-    Tags.set_error_color (Tags.color_of_string current.error_color);
-    Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color);
+    Tags.set_processing_color (Tags.color_of_string processing_color#get);
+    Tags.set_processed_color (Tags.color_of_string processed_color#get);
+    Tags.set_error_color (Tags.color_of_string error_color#get);
+    Tags.set_error_fg_color (Tags.color_of_string error_fg_color#get);
     sn.script#misc#modify_base [`NORMAL, `COLOR clr];
     sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
     sn.messages#refresh_color ();
@@ -871,7 +870,7 @@ let refresh_editor_prefs () =
   List.iter iter_session notebook#pages
 
 let refresh_notebook_pos () =
-  let pos = match prefs.vertical_tabs, prefs.opposite_tabs with
+  let pos = match vertical_tabs#get, opposite_tabs#get with
     | false, false -> `TOP
     | false, true  -> `BOTTOM
     | true , false -> `LEFT
@@ -906,7 +905,7 @@ let toggle_items menu_name l =
   let f d =
     let label = d.Opt.label in
     let k, name = get_shortcut label in
-    let accel = Option.map ((^) prefs.modifier_for_display) k in
+    let accel = Option.map ((^) modifier_for_display#get) k in
     toggle_item name ~label ?accel ~active:d.Opt.init
       ~callback:(printopts_callback d.Opt.opts)
       menu_name
@@ -948,7 +947,7 @@ let alpha_items menu_name item_name l =
     Caveat: the offset is now from the start of the text. *)
 
 let template_item (text, offset, len, key) =
-  let modifier = prefs.modifier_for_templates in
+  let modifier = modifier_for_templates#get in
   let idx = String.index text ' ' in
   let name = String.sub text 0 idx in
   let label = "_"^name^" __" in
@@ -976,7 +975,7 @@ let build_ui () =
   let w = GWindow.window
     ~wm_class:"CoqIde" ~wm_name:"CoqIde"
     ~allow_grow:true ~allow_shrink:true
-    ~width:prefs.window_width ~height:prefs.window_height
+    ~width:window_width#get ~height:window_height#get
     ~title:"CoqIde" ()
   in
   let () =
@@ -1087,9 +1086,9 @@ let build_ui () =
     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"
-      ~active:(prefs.show_toolbar)
+      ~active:(show_toolbar#get)
       ~callback:(fun _ ->
-        prefs.show_toolbar <- not prefs.show_toolbar;
+        show_toolbar#set (not show_toolbar#get);
         !refresh_toolbar_hook ());
     item "Query Pane" ~label:"_Query Pane"
       ~accel:"F1"
@@ -1101,22 +1100,22 @@ let build_ui () =
     item "Navigation" ~label:"_Navigation";
     item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one
       ~tooltip:"Forward one command"
-      ~accel:(prefs.modifier_for_navigation^"Down");
+      ~accel:(modifier_for_navigation#get ^"Down");
     item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one
       ~tooltip:"Backward one command"
-      ~accel:(prefs.modifier_for_navigation^"Up");
+      ~accel:(modifier_for_navigation#get ^"Up");
     item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto
       ~tooltip:"Go to cursor"
-      ~accel:(prefs.modifier_for_navigation^"Right");
+      ~accel:(modifier_for_navigation#get ^"Right");
     item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart
       ~tooltip:"Restart coq"
-      ~accel:(prefs.modifier_for_navigation^"Home");
+      ~accel:(modifier_for_navigation#get ^"Home");
     item "End" ~label:"_End" ~stock:`GOTO_BOTTOM  ~callback:Nav.goto_end
       ~tooltip:"Go to end"
-      ~accel:(prefs.modifier_for_navigation^"End");
+      ~accel:(modifier_for_navigation#get ^"End");
     item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt
       ~tooltip:"Interrupt computations"
-      ~accel:(prefs.modifier_for_navigation^"Break");
+      ~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
@@ -1126,24 +1125,24 @@ let build_ui () =
     item "Previous" ~label:"_Previous" ~stock:`GO_BACK
       ~callback:Nav.previous_occ
       ~tooltip:"Previous occurence"
-      ~accel:(prefs.modifier_for_navigation^"less");
+      ~accel:(modifier_for_navigation#get ^"less");
     item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
       ~tooltip:"Next occurence"
-      ~accel:(prefs.modifier_for_navigation^"greater");
+      ~accel:(modifier_for_navigation#get ^"greater");
     item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
       ~tooltip:"Fully check the document" 
-      ~accel:(current.modifier_for_navigation^"f"); 
+      ~accel:(modifier_for_navigation#get ^"f"); 
   ];
 
   let tacitem s sc =
     item s ~label:("_"^s)
-      ~accel:(prefs.modifier_for_tactics^sc)
+      ~accel:(modifier_for_tactics#get^sc)
       ~callback:(tactic_wizard_callback [s])
   in
   menu tactics_menu [
     item "Try Tactics" ~label:"_Try Tactics";
     item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO
-      ~tooltip:"Proof Wizard" ~accel:(prefs.modifier_for_tactics^"dollar")
+      ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar")
       ~callback:(tactic_wizard_callback prefs.automatic_tactics);
     tacitem "auto" "a";
     tacitem "auto with *" "asterisk";
@@ -1166,7 +1165,7 @@ let build_ui () =
     template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F");
     template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^
                    "with _ := Induction for _ Sort _.\n", 7,10, "S");
-    item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M")
+    item "match" ~label:"match ..." ~accel:(modifier_for_templates#get^"M")
       ~callback:match_callback
   ];
   alpha_items templates_menu "Template" Coq_commands.commands;
@@ -1214,7 +1213,7 @@ let build_ui () =
         browse notebook#current_term.messages#add (doc_url ()));
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add prefs.library_url);
+        browse notebook#current_term.messages#add library_url#get);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ -> on_current_term (fun sn ->
         browse_keyword sn.messages#add (get_current_word sn)));
@@ -1259,7 +1258,7 @@ let build_ui () =
 
   (* Reset on tab switch *)
   let _ = notebook#connect#switch_page ~callback:(fun _ ->
-    if prefs.reset_on_tab_switch then Nav.restart ())
+    if reset_on_tab_switch#get then Nav.restart ())
   in
 
   (* Vertical Separator between Scripts and Goals *)
@@ -1267,7 +1266,7 @@ let build_ui () =
   let () = refresh_notebook_pos () in
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let () = lower_hbox#pack ~expand:true status#coerce in
-  let () = push_info ("Ready"^ if current.nanoPG then ", [μPG]" else "")  in
+  let () = push_info ("Ready"^ if nanoPG#get then ", [μPG]" else "")  in
 
   (* Location display *)
   let l = GMisc.label
@@ -1311,22 +1310,22 @@ let build_ui () =
 
   (* Initializing hooks *)
   let refresh_toolbar () =
-    if prefs.show_toolbar
+    if show_toolbar#get
     then toolbar#misc#show ()
     else toolbar#misc#hide ()
   in
   let refresh_style () =
-    let style =  style_manager#style_scheme prefs.source_style in
+    let style =  style_manager#style_scheme source_style#get 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 prefs.source_language in
+    let lang =  lang_manager#language source_language#get 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:prefs.window_width ~height:prefs.window_height
+    w#resize ~width:window_width#get ~height:window_height#get
   in
   refresh_toolbar ();
   refresh_toolbar_hook := refresh_toolbar;
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index 03b3fcd4e..b8e1861ef 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -87,7 +87,7 @@ object(self)
                 flash_info "Could not overwrite file"
             | _ ->
               Minilib.log "Auto revert set to false";
-              prefs.Preferences.global_auto_revert <- false;
+              Preferences.global_auto_revert#set false;
               revert_timer.kill ()
 
   method save f =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 5892fb3d9..3c5a551c1 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -140,7 +140,7 @@ let filter_coq_files () =  GFile.filter
   ~name:"Coq source code"
   ~patterns:[ "*.v"] ()
 
-let current_dir () = match current.project_path with
+let current_dir () = match project_path#get with
 | None -> ""
 | Some dir -> dir
 
@@ -164,7 +164,7 @@ let select_file_for_open ~title ?filename () =
 	match file_chooser#filename with
 	  | None -> None
 	  | Some _ as f ->
-            current.project_path <- file_chooser#current_folder; f
+            project_path#set file_chooser#current_folder; f
       end
     | `DELETE_EVENT | `CANCEL -> None in
   file_chooser#destroy ();
@@ -193,7 +193,7 @@ let select_file_for_save ~title ?filename () =
         file := file_chooser#filename;
         match !file with
             None -> ()
-          | Some s -> current.project_path <- file_chooser#current_folder
+          | Some s -> project_path#set file_chooser#current_folder
       end
     | `DELETE_EVENT | `CANCEL -> ()
   end ;
@@ -238,7 +238,7 @@ let coqtop_path () =
   let file = match !custom_coqtop with
     | Some s -> s
     | None ->
-      match current.cmd_coqtop with
+      match cmd_coqtop#get with
 	| Some s -> s
 	| None ->
 	  let prog = String.copy Sys.executable_name in
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 805ace935..0668ad09f 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -303,7 +303,7 @@ let init w nb ags =
     then false
     else begin
     eprintf "got key %s\n%!" (pr_key t);
-    if current.nanoPG then begin
+    if nanoPG#get then begin
       match find gui !cur t with
       | `Do e ->
            eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status);
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 08d287138..f8149b4f6 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -38,8 +38,7 @@ object
   method changed = changed#connect ~after
 end
 
-class ['a] preference
-  ~(name : string list) ~(init : 'a) ~(repr : 'a repr) =
+class ['a] preference ~(name : string list) ~(init : 'a) ~(repr : 'a repr) =
 object (self)
   initializer
     let set v = match repr#into v with None -> () | Some s -> self#set s in
@@ -163,42 +162,174 @@ 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 contextual_menus_on_goal_hook = ref (fun x -> ())
 let resize_window_hook = ref (fun () -> ())
 let refresh_tabs_hook = ref (fun () -> ())
 
-type pref =
-    {
-      mutable cmd_coqtop : string option;
-      mutable cmd_coqc : string;
-      mutable cmd_make : string;
-      mutable cmd_coqmakefile : string;
-      mutable cmd_coqdoc : string;
+(** New style preferences *)
+
+let cmd_coqtop =
+  new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string)
+
+let cmd_coqc =
+  new preference ~name:["cmd_coqc"] ~init:"coqc" ~repr:Repr.(string)
+
+let cmd_make =
+  new preference ~name:["cmd_make"] ~init:"make" ~repr:Repr.(string)
+
+let cmd_coqmakefile =
+  new preference ~name:["cmd_coqmakefile"] ~init:"coq_makefile -o makefile *.v" ~repr:Repr.(string)
+
+let cmd_coqdoc =
+  new preference ~name:["cmd_coqdoc"] ~init:"coqdoc -q -g" ~repr:Repr.(string)
+
+let source_language =
+  new preference ~name:["source_language"] ~init:"coq" ~repr:Repr.(string)
+
+let source_style =
+  new preference ~name:["source_style"] ~init:"coq_style" ~repr:Repr.(string)
+
+let global_auto_revert =
+  new preference ~name:["global_auto_revert"] ~init:false ~repr:Repr.(bool)
+
+let global_auto_revert_delay =
+  new preference ~name:["global_auto_revert_delay"] ~init:10000 ~repr:Repr.(int)
+
+let auto_save =
+  new preference ~name:["auto_save"] ~init:true ~repr:Repr.(bool)
+
+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 project_file_name =
+  new preference ~name:["project_file_name"] ~init:"_CoqProject" ~repr:Repr.(string)
+
+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 cmd_print =
+  new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string)
+
+let modifier_for_navigation =
+  new preference ~name:["modifier_for_navigation"] ~init:"<Control><Alt>" ~repr:Repr.(string)
+
+let modifier_for_templates =
+  new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
+ 
+let modifier_for_tactics =
+  new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string)
+
+let modifier_for_display =
+  new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
+
+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 library_url =
+  new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)
+
+let show_toolbar =
+  new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
+
+let contextual_menus_on_goal =
+  new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool)
+
+let window_width =
+  new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int)
+
+let window_height =
+  new preference ~name:["window_height"] ~init:600 ~repr:Repr.(int)
+
+let auto_complete =
+  new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool)
+
+let stop_before =
+  new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool)
+
+let reset_on_tab_switch =
+  new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool)
+
+let vertical_tabs =
+  new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool)
+
+let opposite_tabs =
+  new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool)
+
+let background_color =
+  new preference ~name:["background_color"] ~init:Tags.default_color ~repr:Repr.(string)
+
+let processing_color =
+  new preference ~name:["processing_color"] ~init:Tags.default_processing_color ~repr:Repr.(string)
+
+let processed_color =
+  new preference ~name:["processed_color"] ~init:Tags.default_processed_color ~repr:Repr.(string)
+
+let error_color =
+  new preference ~name:["error_color"] ~init:Tags.default_error_color ~repr:Repr.(string)
+
+let error_fg_color =
+  new preference ~name:["error_fg_color"] ~init:Tags.default_error_fg_color ~repr:Repr.(string)
+
+let dynamic_word_wrap =
+  new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool)
+
+let show_line_number =
+  new preference ~name:["show_line_number"] ~init:false ~repr:Repr.(bool)
+
+let auto_indent =
+  new preference ~name:["auto_indent"] ~init:false ~repr:Repr.(bool)
+
+let show_spaces =
+  new preference ~name:["show_spaces"] ~init:true ~repr:Repr.(bool)
 
-      mutable source_language : string;
-      mutable source_style : string;
+let show_right_margin =
+  new preference ~name:["show_right_margin"] ~init:false ~repr:Repr.(bool)
 
-      mutable global_auto_revert : bool;
-      mutable global_auto_revert_delay : int;
+let show_progress_bar =
+  new preference ~name:["show_progress_bar"] ~init:true ~repr:Repr.(bool)
+
+let spaces_instead_of_tabs =
+  new preference ~name:["spaces_instead_of_tabs"] ~init:true ~repr:Repr.(bool)
+
+let tab_length =
+  new preference ~name:["tab_length"] ~init:2 ~repr:Repr.(int)
+
+let highlight_current_line =
+  new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool)
+
+let nanoPG =
+  new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool)
+
+(** Old style preferences *)
+
+type pref =
+    {
 
-      mutable auto_save : bool;
-      mutable auto_save_delay : int;
       mutable auto_save_name : string * string;
 
       mutable read_project : project_behavior;
-      mutable project_file_name : string;
-      mutable project_path : string option;
 
       mutable encoding : inputenc;
 
       mutable automatic_tactics : string list;
-      mutable cmd_print : string;
-
-      mutable modifier_for_navigation : string;
-      mutable modifier_for_templates : string;
-      mutable modifier_for_tactics : string;
-      mutable modifier_for_display : string;
-      mutable modifiers_valid : string;
 
       mutable cmd_browse : string;
       mutable cmd_editor : string;
@@ -206,79 +337,22 @@ type pref =
       mutable text_font : Pango.font_description;
 
       mutable doc_url : string;
-      mutable library_url : string;
-
-      mutable show_toolbar : bool;
-      mutable contextual_menus_on_goal : bool;
-      mutable window_width : int;
-      mutable window_height :int;
-      mutable query_window_width : int;
-      mutable query_window_height : int;
-(*
-      mutable use_utf8_notation : bool;
-*)
-      mutable auto_complete : bool;
-      mutable stop_before : bool;
-      mutable reset_on_tab_switch : bool;
-      mutable vertical_tabs : bool;
-      mutable opposite_tabs : bool;
-
-      mutable background_color : string;
-      mutable processing_color : string;
-      mutable processed_color : string;
-      mutable error_color : string;
-      mutable error_fg_color : string;
-
-      mutable dynamic_word_wrap : bool;
-      mutable show_line_number : bool;
-      mutable auto_indent : bool;
-      mutable show_spaces : bool;
-      mutable show_right_margin : bool;
-      mutable show_progress_bar : bool;
-      mutable spaces_instead_of_tabs : bool;
-      mutable tab_length : int;
-      mutable highlight_current_line : bool;
-
-      mutable nanoPG : bool;
 
 }
 
 let use_default_doc_url = "(automatic)"
 
 let current = {
-    cmd_coqtop = None;
-    cmd_coqc = "coqc";
-    cmd_make = "make";
-    cmd_coqmakefile = "coq_makefile -o makefile *.v";
-    cmd_coqdoc = "coqdoc -q -g";
-    cmd_print = "lpr";
-
-    global_auto_revert = false;
-    global_auto_revert_delay = 10000;
-
-    auto_save = true;
-    auto_save_delay = 10000;
-    auto_save_name = "#","#";
 
-    source_language = "coq";
-    source_style = "coq_style";
+    auto_save_name = "#","#";
 
     read_project = Append_args;
-    project_file_name = "_CoqProject";
-    project_path = None;
 
     encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale;
 
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
 
-    modifier_for_navigation = "<Control><Alt>";
-    modifier_for_templates = "<Control><Shift>";
-    modifier_for_tactics = "<Control><Alt>";
-    modifier_for_display = "<Alt><Shift>";
-    modifiers_valid = "<Alt><Control><Shift>";
-
-
     cmd_browse = Flags.browser_cmd_fmt;
     cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s";
 
@@ -288,40 +362,6 @@ let current = {
 					  |_ -> "Monospace 10");
 
     doc_url = Coq_config.wwwrefman;
-    library_url = Coq_config.wwwstdlib;
-
-    show_toolbar = true;
-    contextual_menus_on_goal = true;
-    window_width = 800;
-    window_height = 600;
-    query_window_width = 600;
-    query_window_height = 400;
-(*
-    use_utf8_notation = false;
-*)
-    auto_complete = false;
-    stop_before = true;
-    reset_on_tab_switch = false;
-    vertical_tabs = false;
-    opposite_tabs = false;
-
-    background_color = Tags.default_color;
-    processed_color = Tags.default_processed_color;
-    processing_color = Tags.default_processing_color;
-    error_color = Tags.default_error_color;
-    error_fg_color = Tags.default_error_fg_color;
-
-    dynamic_word_wrap = false;
-    show_line_number = false;
-    auto_indent = false;
-    show_spaces = true;
-    show_right_margin = false;
-    show_progress_bar = true;
-    spaces_instead_of_tabs = true;
-    tab_length = 2;
-    highlight_current_line = false;
-
-    nanoPG = false;
   }
 
 let save_pref () =
@@ -334,67 +374,19 @@ let save_pref () =
   let fold key obj accu = add key (obj.get ()) accu in
  
     (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++
-    add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
-    add "cmd_coqc" [p.cmd_coqc] ++
-    add "cmd_make" [p.cmd_make] ++
-    add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
-    add "cmd_coqdoc" [p.cmd_coqdoc] ++
-    add "source_language" [p.source_language] ++
-    add "source_style" [p.source_style] ++
-    add "global_auto_revert" [string_of_bool p.global_auto_revert] ++
-    add "global_auto_revert_delay"
-      [string_of_int p.global_auto_revert_delay] ++
-    add "auto_save" [string_of_bool p.auto_save] ++
-    add "auto_save_delay" [string_of_int p.auto_save_delay] ++
     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 "project_file_name" [p.project_file_name] ++
-    add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++
 
     add "encoding" [string_of_inputenc p.encoding] ++
 
     add "automatic_tactics" p.automatic_tactics ++
-    add "cmd_print" [p.cmd_print] ++
-    add "modifier_for_navigation" [p.modifier_for_navigation] ++
-    add "modifier_for_templates" [p.modifier_for_templates] ++
-    add "modifier_for_tactics" [p.modifier_for_tactics] ++
-    add "modifier_for_display" [p.modifier_for_display] ++
-    add "modifiers_valid" [p.modifiers_valid] ++
     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] ++
-    add "library_url" [p.library_url] ++
-    add "show_toolbar" [string_of_bool p.show_toolbar] ++
-    add "contextual_menus_on_goal"
-      [string_of_bool p.contextual_menus_on_goal] ++
-    add "window_height" [string_of_int p.window_height] ++
-    add "window_width" [string_of_int p.window_width] ++
-    add "query_window_height" [string_of_int p.query_window_height] ++
-    add "query_window_width" [string_of_int p.query_window_width] ++
-    add "auto_complete" [string_of_bool p.auto_complete] ++
-    add "stop_before" [string_of_bool p.stop_before] ++
-    add "reset_on_tab_switch" [string_of_bool p.reset_on_tab_switch] ++
-    add "vertical_tabs" [string_of_bool p.vertical_tabs] ++
-    add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
-    add "background_color" [p.background_color] ++
-    add "processing_color" [p.processing_color] ++
-    add "processed_color" [p.processed_color] ++
-    add "error_color" [p.error_color] ++
-    add "error_fg_color" [p.error_fg_color] ++
-    add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++
-    add "show_line_number" [string_of_bool p.show_line_number] ++
-    add "auto_indent" [string_of_bool p.auto_indent] ++
-    add "show_spaces" [string_of_bool p.show_spaces] ++
-    add "show_right_margin" [string_of_bool p.show_right_margin] ++
-    add "show_progress_bar" [string_of_bool p.show_progress_bar] ++
-    add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++
-    add "tab_length" [string_of_int p.tab_length] ++
-    add "highlight_current_line" [string_of_bool p.highlight_current_line] ++
-    add "nanoPG" [string_of_bool p.nanoPG] ++
     Config_lexer.print_file pref_file
 
 let load_pref () =
@@ -409,45 +401,16 @@ let load_pref () =
     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_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
-    let set_int k f = set_hd k (fun v -> f (int_of_string 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
-    let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ ->  Some h)) in
-    set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v);
-    set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
-    set_hd "cmd_make" (fun v -> np.cmd_make <- v);
-    set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
-    set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v);
-    set_hd "source_language" (fun v -> np.source_language <- v);
-    set_hd "source_style" (fun v -> np.source_style <- v);
-    set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v);
-    set_int "global_auto_revert_delay"
-      (fun v -> np.global_auto_revert_delay <- v);
-    set_bool "auto_save" (fun v -> np.auto_save <- v);
-    set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
     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_hd "project_file_name" (fun v -> np.project_file_name <- v);
-    set_option "project_path" (fun v -> np.project_path <- v);
     set "automatic_tactics"
       (fun v -> np.automatic_tactics <- v);
-    set_hd "cmd_print" (fun v -> np.cmd_print <- v);
-    set_hd "modifier_for_navigation"
-      (fun v -> np.modifier_for_navigation <- v);
-    set_hd "modifier_for_templates"
-      (fun v -> np.modifier_for_templates <- v);
-    set_hd "modifier_for_tactics"
-      (fun v -> np.modifier_for_tactics <- v);
-    set_hd "modifier_for_display"
-      (fun v -> np.modifier_for_display <- v);
-    set_hd "modifiers_valid"
-      (fun v ->
-	np.modifiers_valid <- 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);
@@ -460,61 +423,21 @@ let load_pref () =
       then
 	(* ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*)
       np.doc_url <- v);
-    set_hd "library_url" (fun v -> np.library_url <- v);
-    set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
-    set_bool "contextual_menus_on_goal"
-      (fun v -> np.contextual_menus_on_goal <- v);
-    set_int "window_width" (fun v -> np.window_width <- v);
-    set_int "window_height" (fun v -> np.window_height <- v);
-    set_int "query_window_width" (fun v -> np.query_window_width <- v);
-    set_int "query_window_height" (fun v -> np.query_window_height <- v);
-    set_bool "auto_complete" (fun v -> np.auto_complete <- v);
-    set_bool "stop_before" (fun v -> np.stop_before <- v);
-    set_bool "reset_on_tab_switch" (fun v -> np.reset_on_tab_switch <- v);
-    set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v);
-    set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
-    set_hd "background_color" (fun v -> np.background_color <- v);
-    set_hd "processing_color" (fun v -> np.processing_color <- v);
-    set_hd "processed_color" (fun v -> np.processed_color <- v);
-    set_hd "error_color" (fun v -> np.error_color <- v);
-    set_hd "error_fg_color" (fun v -> np.error_fg_color <- v);
-    set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v);
-    set_bool "show_line_number" (fun v -> np.show_line_number <- v);
-    set_bool "auto_indent" (fun v -> np.auto_indent <- v);
-    set_bool "show_spaces" (fun v -> np.show_spaces <- v);
-    set_bool "show_right_margin" (fun v -> np.show_right_margin <- v);
-    set_bool "show_progress_bar" (fun v -> np.show_progress_bar <- v);
-    set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v);
-    set_int "tab_length" (fun v -> np.tab_length <- v);
-    set_bool "highlight_current_line" (fun v -> np.highlight_current_line <- v);
-    set_bool "nanoPG" (fun v -> np.nanoPG <- v);
     ()
 
+let pstring name p = string ~f:p#set name p#get
+let pbool name p = bool ~f:p#set name p#get
+
 let configure ?(apply=(fun () -> ())) () =
   let cmd_coqtop =
     string
-      ~f:(fun s -> current.cmd_coqtop <- if s = "AUTO" then None else Some s)
-      "       coqtop" (match current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in
-  let cmd_coqc =
-    string
-      ~f:(fun s -> current.cmd_coqc <- s)
-      "       coqc"  current.cmd_coqc in
-  let cmd_make =
-    string
-      ~f:(fun s -> current.cmd_make <- s)
-      "       make" current.cmd_make in
-  let cmd_coqmakefile =
-    string
-      ~f:(fun s -> current.cmd_coqmakefile <- s)
-      "coqmakefile" current.cmd_coqmakefile in
-  let cmd_coqdoc =
-    string
-      ~f:(fun s -> current.cmd_coqdoc <- s)
-      "     coqdoc" current.cmd_coqdoc in
-  let cmd_print =
-    string
-      ~f:(fun s -> current.cmd_print <- s)
-      "   Print ps" current.cmd_print in
+      ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
+      "       coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
+  let cmd_coqc = pstring "       coqc" cmd_coqc in
+  let cmd_make = pstring "       make" cmd_make in
+  let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in
+  let cmd_coqdoc = pstring "     coqdoc" cmd_coqdoc in
+  let cmd_print = pstring "   Print ps" cmd_print in
 
   let config_font =
     let box = GPack.hbox () in
@@ -572,7 +495,7 @@ let configure ?(apply=(fun () -> ())) () =
     let () = error_label#set_xalign 0. in
     let () = error_fg_label#set_xalign 0. in
     let background_button = GButton.color_button
-      ~color:(Tags.color_of_string (current.background_color))
+      ~color:(Tags.color_of_string (background_color#get))
       ~packing:(table#attach ~left:1 ~top:0) ()
     in
     let processed_button = GButton.color_button
@@ -604,11 +527,11 @@ let configure ?(apply=(fun () -> ())) () =
     let _ = reset_button#connect#clicked ~callback:reset_cb in
     let label = "Color configuration" in
     let callback () =
-      current.background_color <- Tags.string_of_color background_button#color;
-      current.processing_color <- Tags.string_of_color processing_button#color;
-      current.processed_color <- Tags.string_of_color processed_button#color;
-      current.error_color <- Tags.string_of_color error_button#color;
-      current.error_fg_color <- Tags.string_of_color error_fg_button#color;
+      background_color#set (Tags.string_of_color background_button#color);
+      processing_color#set (Tags.string_of_color processing_button#color);
+      processed_color#set (Tags.string_of_color processed_button#color);
+      error_color#set (Tags.string_of_color error_button#color);
+      error_fg_color#set (Tags.string_of_color error_fg_button#color);
       !refresh_editor_hook ();
       Tags.set_processing_color processing_button#color;
       Tags.set_processed_color processed_button#color;
@@ -623,22 +546,22 @@ let configure ?(apply=(fun () -> ())) () =
     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" current.dynamic_word_wrap in
-    let line = gen_button "Show line number" current.show_line_number in
-    let auto_indent = gen_button "Auto indentation" current.auto_indent in
-    let auto_complete = gen_button "Auto completion" current.auto_complete in
-    let show_spaces = gen_button "Show spaces" current.show_spaces in
-    let show_right_margin = gen_button "Show right margin" current.show_right_margin in
-    let show_progress_bar = gen_button "Show progress bar" current.show_progress_bar in
-    let spaces_instead_of_tabs =
+    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"
-      current.spaces_instead_of_tabs
+      spaces_instead_of_tabs#get
     in
-    let highlight_current_line =
+    let b_highlight_current_line =
       gen_button "Highlight current line"
-      current.highlight_current_line
+      highlight_current_line#get
     in
-    let nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" current.nanoPG 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. *)
@@ -648,17 +571,17 @@ let configure ?(apply=(fun () -> ())) () =
 (*       ~digits:0 ~packing:lbox#pack () *)
 (*     in *)
     let callback () =
-      current.dynamic_word_wrap <- wrap#active;
-      current.show_line_number <- line#active;
-      current.auto_indent <- auto_indent#active;
-      current.show_spaces <- show_spaces#active;
-      current.show_right_margin <- show_right_margin#active;
-      current.show_progress_bar <- show_progress_bar#active;
-      current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active;
-      current.highlight_current_line <- highlight_current_line#active;
-      current.nanoPG <- nanoPG#active;
-      current.auto_complete <- auto_complete#active;
-(*       current.tab_length <- tab_width#value_as_int; *)
+      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 ()
     in
     custom ~label box callback true
@@ -688,66 +611,34 @@ let configure ?(apply=(fun () -> ())) () =
       (string_of_int current.window_width)
   in
 *)
-(*  let use_utf8_notation =
-    bool
-      ~f:(fun b ->
-	    current.use_utf8_notation <- b;
-	 )
-      "Use Unicode Notation: " current.use_utf8_notation
-  in
-*)
 (*
   let config_appearance = [show_toolbar; window_width; window_height] in
 *)
-  let global_auto_revert =
-    bool
-      ~f:(fun s -> current.global_auto_revert <- s)
-      "Enable global auto revert" current.global_auto_revert
-  in
+  let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in
   let global_auto_revert_delay =
     string
-    ~f:(fun s -> current.global_auto_revert_delay <-
+    ~f:(fun s -> global_auto_revert_delay#set
 	  (try int_of_string s with _ -> 10000))
       "Global auto revert delay (ms)"
-      (string_of_int current.global_auto_revert_delay)
+      (string_of_int global_auto_revert_delay#get)
   in
 
-  let auto_save =
-    bool
-      ~f:(fun s -> current.auto_save <- s)
-      "Enable auto save" current.auto_save
-  in
+  let auto_save = pbool "Enable auto save" auto_save in
   let auto_save_delay =
     string
-    ~f:(fun s -> current.auto_save_delay <-
+    ~f:(fun s -> auto_save_delay#set
 	  (try int_of_string s with _ -> 10000))
       "Auto save delay (ms)"
-      (string_of_int current.auto_save_delay)
+      (string_of_int auto_save_delay#get)
   in
 
-  let stop_before =
-    bool
-      ~f:(fun s -> current.stop_before <- s)
-      "Stop interpreting before the current point" current.stop_before
-  in
+  let stop_before = pbool "Stop interpreting before the current point" stop_before in
 
-  let reset_on_tab_switch =
-    bool
-      ~f:(fun s -> current.reset_on_tab_switch <- s)
-      "Reset coqtop on tab switch" current.reset_on_tab_switch
-  in
+  let reset_on_tab_switch = pbool "Reset coqtop on tab switch" reset_on_tab_switch in
 
-  let vertical_tabs =
-    bool
-      ~f:(fun s -> current.vertical_tabs <- s; !refresh_tabs_hook ())
-      "Vertical tabs" current.vertical_tabs
-  in
+  let vertical_tabs = pbool "Vertical tabs" vertical_tabs in
 
-  let opposite_tabs =
-    bool
-      ~f:(fun s -> current.opposite_tabs <- s; !refresh_tabs_hook ())
-      "Tabs on opposite side" current.opposite_tabs
-  in
+  let opposite_tabs = pbool "Tabs on opposite side" opposite_tabs in
 
   let encodings =
     combo
@@ -763,17 +654,17 @@ let configure ?(apply=(fun () -> ())) () =
 
   let source_style =
     let f s =
-      current.source_style <- s;
+      source_style#set s;
       !refresh_style_hook ()
     in
     combo "Highlighting style:"
       ~f ~new_allowed:false
-      style_manager#style_scheme_ids current.source_style
+      style_manager#style_scheme_ids source_style#get
   in
 
   let source_language =
     let f s =
-      current.source_language <- s;
+      source_language#set s;
       !refresh_language_hook ()
     in
     combo "Language:"
@@ -781,7 +672,7 @@ let configure ?(apply=(fun () -> ())) () =
       (List.filter
         (fun x -> Str.string_match (Str.regexp "^coq") x 0)
         lang_manager#language_ids)
-      current.source_language
+      source_language#get
   in
 
   let read_project =
@@ -794,51 +685,47 @@ let configure ?(apply=(fun () -> ())) () =
        string_of_project_behavior Ignore_args]
       (string_of_project_behavior current.read_project)
   in
-  let project_file_name =
-    string "Default name for project file"
-      ~f:(fun s -> current.project_file_name <- s)
-      current.project_file_name
-  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 current.modifiers_valid 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 -> current.modifier_for_tactics <- mod_list_to_str l)
+      ~f:(fun l -> modifier_for_tactics#set (mod_list_to_str l))
       ~help:help_string
       "Modifiers for Tactics Menu"
-      (str_to_mod_list current.modifier_for_tactics)
+      (str_to_mod_list modifier_for_tactics#get)
   in
   let modifier_for_templates =
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
+      ~f:(fun l -> modifier_for_templates#set (mod_list_to_str l))
       ~help:help_string
       "Modifiers for Templates Menu"
-      (str_to_mod_list current.modifier_for_templates)
+      (str_to_mod_list modifier_for_templates#get)
   in
   let modifier_for_navigation =
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
+      ~f:(fun l -> modifier_for_navigation#set (mod_list_to_str l))
       ~help:help_string
       "Modifiers for Navigation Menu"
-      (str_to_mod_list current.modifier_for_navigation)
+      (str_to_mod_list modifier_for_navigation#get)
   in
   let modifier_for_display =
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
+      ~f:(fun l -> modifier_for_display#set (mod_list_to_str l))
       ~help:help_string
       "Modifiers for View Menu"
-      (str_to_mod_list current.modifier_for_display)
+      (str_to_mod_list modifier_for_display#get)
   in
   let modifiers_valid =
     modifiers
       ~f:(fun l ->
-	current.modifiers_valid <- mod_list_to_str l)
+	modifiers_valid#set (mod_list_to_str l))
       "Allowed modifiers"
       the_valid_mod
   in
@@ -890,11 +777,11 @@ let configure ?(apply=(fun () -> ())) () =
     ] in
     combo
       "Library URL"
-      ~f:(fun s -> current.library_url <- s)
+      ~f:(fun s -> library_url#set s)
       ~new_allowed: true
-      (predefined@[if List.mem current.library_url predefined then ""
-                   else current.library_url])
-      current.library_url
+      (predefined@[if List.mem library_url#get predefined then ""
+                   else library_url#get])
+      library_url#get
   in
   let automatic_tactics =
     strings
@@ -905,13 +792,7 @@ let configure ?(apply=(fun () -> ())) () =
 
   in
 
-  let contextual_menus_on_goal =
-    bool
-      ~f:(fun s ->
-	    current.contextual_menus_on_goal <- s;
-	    !contextual_menus_on_goal_hook s)
-      "Contextual menus on goal" current.contextual_menus_on_goal
-  in
+  let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
 
   let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
               vertical_tabs;opposite_tabs] in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 8e1d926ac..0a83e609b 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -31,80 +31,69 @@ object
   method set : 'a -> unit
 end
 
+val cmd_coqtop : string option preference
+val cmd_coqc : string preference
+val cmd_make : string preference
+val cmd_coqmakefile : string preference
+val cmd_coqdoc : string preference
+val source_language : string preference
+val source_style : string preference
+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 project_file_name : string preference
+val project_path : string option 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 library_url : string preference
+val show_toolbar : bool preference
+val contextual_menus_on_goal : bool preference
+val window_width : int preference
+val window_height : int preference
+val auto_complete : bool preference
+val stop_before : bool preference
+val reset_on_tab_switch : bool preference
+val vertical_tabs : bool preference
+val opposite_tabs : bool preference
+val background_color : string preference
+val processing_color : string preference
+val processed_color : string preference
+val error_color : string preference
+val error_fg_color : string preference
+val dynamic_word_wrap : bool preference
+val show_line_number : bool preference
+val auto_indent : bool preference
+val show_spaces : bool preference
+val show_right_margin : bool preference
+val show_progress_bar : bool preference
+val spaces_instead_of_tabs : bool preference
+val tab_length : int preference
+val highlight_current_line : bool preference
+val nanoPG : bool preference
+
 type pref =
     {
-      mutable cmd_coqtop : string option;
-      mutable cmd_coqc : string;
-      mutable cmd_make : string;
-      mutable cmd_coqmakefile : string;
-      mutable cmd_coqdoc : string;
-
-      mutable source_language : string;
-      mutable source_style : string;
-
-      mutable global_auto_revert : bool;
-      mutable global_auto_revert_delay : int;
-
-      mutable auto_save : bool;
-      mutable auto_save_delay : int;
       mutable auto_save_name : string * string;
-
       mutable read_project : project_behavior;
-      mutable project_file_name : string;
-      mutable project_path : string option;
-
       mutable encoding : inputenc;
-
       mutable automatic_tactics : string list;
-      mutable cmd_print : string;
-
-      mutable modifier_for_navigation : string;
-      mutable modifier_for_templates : string;
-      mutable modifier_for_tactics : string;
-      mutable modifier_for_display : string;
-      mutable modifiers_valid : string;
-
       mutable cmd_browse : string;
       mutable cmd_editor : string;
-
       mutable text_font : Pango.font_description;
-
       mutable doc_url : string;
-      mutable library_url : string;
-
-      mutable show_toolbar : bool;
-      mutable contextual_menus_on_goal : bool;
-      mutable window_width : int;
-      mutable window_height : int;
-      mutable query_window_width : int;
-      mutable query_window_height : int;
-(*
-      mutable use_utf8_notation : bool;
-*)
-      mutable auto_complete : bool;
-      mutable stop_before : bool;
-      mutable reset_on_tab_switch : bool;
-      mutable vertical_tabs : bool;
-      mutable opposite_tabs : bool;
-
-      mutable background_color : string;
-      mutable processing_color : string;
-      mutable processed_color : string;
-      mutable error_color : string;
-      mutable error_fg_color : string;
-
-      mutable dynamic_word_wrap : bool;
-      mutable show_line_number : bool;
-      mutable auto_indent : bool;
-      mutable show_spaces : bool;
-      mutable show_right_margin : bool;
-      mutable show_progress_bar : bool;
-      mutable spaces_instead_of_tabs : bool;
-      mutable tab_length : int;
-      mutable highlight_current_line : bool;
-
-      mutable nanoPG : bool;
-
     }
 
 val save_pref : unit -> unit
diff --git a/ide/session.ml b/ide/session.ml
index a795f6331..0b26c1f65 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -50,8 +50,8 @@ let create_buffer () =
   let buffer = GSourceView2.source_buffer
     ~tag_table:Tags.Script.table
     ~highlight_matching_brackets:true
-    ?language:(lang_manager#language prefs.source_language)
-    ?style_scheme:(style_manager#style_scheme prefs.source_style)
+    ?language:(lang_manager#language source_language#get)
+    ?style_scheme:(style_manager#style_scheme source_style#get)
     ()
   in
   let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
@@ -255,7 +255,7 @@ let make_table_widget ?sort cd cb =
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
   let refresh () =
-    let clr = Tags.color_of_string current.background_color in
+    let clr = Tags.color_of_string background_color#get in
     data#misc#modify_base [`NORMAL, `COLOR clr]
   in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 7dad92ed6..bf25ddfa1 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -86,7 +86,7 @@ object(self)
     let result = GText.view ~packing:r_bin#add () in
     views <- (frame#coerce, result, combo#entry) :: views;
     result#misc#modify_font current.text_font;
-    let clr = Tags.color_of_string current.background_color in
+    let clr = Tags.color_of_string background_color#get in
     result#misc#modify_base [`NORMAL, `COLOR clr];
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
@@ -150,7 +150,7 @@ object(self)
     List.iter iter views
 
   method refresh_color () =
-    let clr = Tags.color_of_string current.background_color in
+    let clr = Tags.color_of_string background_color#get in
     let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
     List.iter iter views
 
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 211db537e..3fff01945 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -86,7 +86,7 @@ let message_view () : message_view =
 
     method refresh_color () =
       let open Preferences in
-      let clr = Tags.color_of_string current.background_color in
+      let clr = Tags.color_of_string background_color#get in
       view#misc#modify_base [`NORMAL, `COLOR clr]
 
   end