Simplifying CoqIDE preferences mechanism.

We use a class-based system instead of the old record-based system. This
allows for more uniformity and the possibility to define complex
interactions with preferences based on GTK signals. This will allow to
simplify some architectural choices.

3 files changed, 112 insertions, 5 deletions

diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 87cc6d06e..367153568 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -17,7 +17,7 @@
 
 let space = [' ' '\010' '\013' '\009' '\012']
 let char = ['A'-'Z' 'a'-'z' '_' '0'-'9']
-let ident = char+
+let ident = (char | '.')+
 let ignore = space | ('#' [^ '\n']*)
 
 rule prefs m = parse
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c59642d3a..08d287138 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -17,6 +17,88 @@ let style_manager = GSourceView2.source_style_scheme_manager ~default:true
 let () = style_manager#set_search_path
   ((Minilib.coqide_data_dirs ())@style_manager#search_path)
 
+(** Generic preferences *)
+
+type obj = {
+  set : string list -> unit;
+  get : unit -> string list;
+}
+
+let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty
+
+class type ['a] repr =
+object
+  method into : string list -> 'a option
+  method from : 'a -> string list
+end
+
+class ['a] preference_signals ~(changed : 'a GUtil.signal) =
+object
+  inherit GUtil.ml_signals [changed#disconnect]
+  method changed = changed#connect ~after
+end
+
+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
+    let get () = repr#from self#get in
+    let obj = { set = set; get = get; } in
+    let name = String.concat "." name in
+    if Util.String.Map.mem name !preferences then
+      invalid_arg ("Preference " ^ name ^ " already exists")
+    else
+      preferences := Util.String.Map.add name obj !preferences
+
+  val default = init
+  val mutable data = init
+  val changed : 'a GUtil.signal = new GUtil.signal ()
+  val name : string list = name
+  method connect = new preference_signals ~changed
+  method get = data
+  method set (n : 'a) = data <- n; changed#call n
+end
+
+(** Useful marshallers *)
+
+module Repr =
+struct
+
+let string : string repr =
+object
+  method from s = [s]
+  method into = function [s] -> Some s | _ -> None
+end
+
+let bool : bool repr =
+object
+  method from s = [string_of_bool s]
+  method into = function
+  | ["true"] -> Some true
+  | ["false"] -> Some false
+  | _ -> None
+end
+
+let int : int repr =
+object
+  method from s = [string_of_int s]
+  method into = function
+  | [i] -> (try Some (int_of_string i) with _ -> None)
+  | _ -> None
+end
+
+let option (r : 'a repr) : 'a option repr =
+object
+  method from = function None -> [] | Some v -> "" :: r#from v
+  method into = function
+  | [] -> Some None
+  | "" :: s -> Some (r#into s)
+  | _ -> None
+end
+
+end
+
 let get_config_file name =
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
   let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in
@@ -247,10 +329,11 @@ let save_pref () =
   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
-    Util.String.Map.empty ++
+  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 "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
@@ -318,6 +401,11 @@ let load_pref () =
   let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
 
     let m = Config_lexer.load_file loaded_pref_file in
+    let iter name v =
+      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
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1e4f152c2..8e1d926ac 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -12,6 +12,25 @@ val style_manager : GSourceView2.source_style_scheme_manager
 type project_behavior = Ignore_args | Append_args | Subst_args
 type inputenc = Elocale | Eutf8 | Emanual of string
 
+class type ['a] repr =
+object
+  method into : string list -> 'a option
+  method from : 'a -> string list
+end
+
+class ['a] preference_signals : changed:'a GUtil.signal ->
+object
+  inherit GUtil.ml_signals
+  method changed : callback:('a -> unit) -> GtkSignal.id
+end
+
+class ['a] preference : name:string list -> init:'a -> repr:'a repr ->
+object
+  method connect : 'a preference_signals
+  method get : 'a
+  method set : 'a -> unit
+end
+
 type pref =
     {
       mutable cmd_coqtop : string option;