fichier de pref coq IDE en ASCII (ENFIN)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3963 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 153 insertions, 157 deletions

diff --git a/ide/.cvsignore b/ide/.cvsignore
index 331b1947b..56eea49c9 100644
--- a/ide/.cvsignore
+++ b/ide/.cvsignore
@@ -8,3 +8,5 @@ Makefile
 test
 config_lexer.ml
 *.crashcoqide
+config_parser.mli
+config_parser.ml
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 0d0e6307e..480f04e24 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -1,60 +1,58 @@
 {
 
   open Lexing
+  open Format
+  open Config_parser
+  open Util
+
+  let string_buffer = Buffer.create 1024
+
 }
 
-let space = 
-  [' ' '\010' '\013' '\009' '\012']
+let space = [' ' '\010' '\013' '\009' '\012']
 let char = ['A'-'Z' 'a'-'z' '_' '0'-'9']
-
 let ident = char+
 
-let value = ('"'|'[')( [^ '='] | ('\\''"') )*('"'|']')
-let list_value = [^';']+ ';'
-
-rule next_config = parse
-  | ident 
-      { let id = lexeme lexbuf in 
-        let v = value lexbuf in
-        (id,v)
-      }
-  | _    { next_config lexbuf}
-  | eof  { raise End_of_file }
-
-and value = parse
-  | value { let s = lexeme lexbuf in
-	    String.sub s 1 (String.length s - 2)}
-  | _    { value lexbuf }
-  | eof  { raise End_of_file }
-
-and split_list = parse
-  | list_value {
-      let h = lexeme lexbuf in
-      h::(split_list lexbuf)
-    }
-  | _ { split_list lexbuf}
-  | eof {[]}
+rule token = parse
+  | space+        { token lexbuf }
+  | '#' [^ '\n']* { token lexbuf }
+  | ident { IDENT (lexeme lexbuf) }
+  | '='   { EQUAL }
+  | '"'   { Buffer.reset string_buffer; 
+	    Buffer.add_char string_buffer '"';
+	    string lexbuf;
+	    let s = Buffer.contents string_buffer in
+	    STRING (Scanf.sscanf s "%S" (fun s -> s)) }
+  | _     { let c = lexeme_start lexbuf in
+	    eprintf ".coqiderc: invalid character (%d)\n@." c; 
+	    token lexbuf }
+  | eof   { EOF }
+
+and string = parse
+  | '"'  { Buffer.add_char string_buffer '"' }
+  | '\\' '"' | _ 
+         { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
+  | eof  { eprintf ".coqiderc: unterminated string\n@." }
 
 {
-  let get_config f = 
-    let ci = open_in f in
-    let lb = from_channel ci in 
-    let result = ref [] in
-    begin try 
-      while true do 
-	let r = next_config lb in
-	result := r::!result
-      done
-    with End_of_file -> close_in ci; 
-    end;
-    !result
-
-  let split s = 
-    let cs = ref "" in
-    let l = ref [] in
-    String.iter 
-      (fun c -> if c = ';' then begin l:= !cs::!l; cs:="" end 
-       else cs := !cs^(Char.escaped c))
-      s;
-    if !cs ="" then !l else !cs::!l
+
+  let load_file f =
+    let c = open_in f in
+    let lb = from_channel c in
+    let m = Config_parser.prefs token lb in
+    close_in c;
+    m
+
+  let print_file f m =
+    let c = open_out f in
+    let fmt = formatter_of_out_channel c in
+    let rec print_list fmt = function
+      | [] -> ()
+      | s :: sl -> fprintf fmt "%S@ %a" s print_list sl
+    in
+    Stringmap.iter 
+      (fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
+    fprintf fmt "@.";
+    close_out c
+
 }
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
new file mode 100644
index 000000000..fe9071964
--- /dev/null
+++ b/ide/config_parser.mly
@@ -0,0 +1,34 @@
+
+%{
+
+  open Parsing
+  open Util
+
+%}
+
+%token <string> IDENT STRING
+%token EQUAL EOF
+
+%type <(string list) Util.Stringmap.t> prefs
+%start prefs
+
+%%
+
+prefs:
+  pref_list EOF { $1 }
+;
+
+pref_list:
+   pref_list pref { let (k,d) = $2 in Stringmap.add k d $1 }
+ | /* epsilon */  { Stringmap.empty }
+;
+
+pref:
+  IDENT EQUAL string_list { ($1, List.rev $3) }
+;
+
+string_list:
+   string_list STRING { $2 :: $1 }
+ | /* epsilon */      { [] }
+;
+
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d5d1490fe..f0f54650e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -200,3 +200,5 @@ let find_tag_limits (tag :GText.tag) (it:GText.iter) =
 
 let async = 
   if Sys.os_type <> "Unix" then GtkThread.async else (fun x -> x)
+
+
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c78cf3214..4370ca985 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,5 +1,6 @@
 open Configwin
 open Printf
+open Util
 
 let pref_file = 
   try (Filename.concat (Sys.getenv "HOME") ".coqidepref")
@@ -50,7 +51,7 @@ type pref =
 
       mutable auto_save : bool;
       mutable auto_save_delay : int;
-      mutable auto_save_name : string*string;
+      mutable auto_save_name : string * string;
 
       mutable automatic_tactics : (string * string) list;
       mutable cmd_print : string;
@@ -68,61 +69,34 @@ type pref =
 
 let save_pref p =
   try 
-    let fd = open_out pref_file in
-    output_value fd p;
-(*
-    let output_string f c = fprintf fd "%s = \"%s\"\n" f c in
-    let output_bool f c = fprintf fd "%s = \"%b\"\n" f c in
-    let output_int f c = fprintf fd "%s = \"%d\"\n" f c in
-    let output_list f to_string l = 
-      fprintf fd "%s = [%a]\n" f 
-	(fun c -> 
-	   List.iter
-	   (fun x -> fprintf c "%a;" to_string x)) l in
-    let output_modi fd m = fprintf fd "%s" (mod_to_str m) in
-    let output_tactics fd (m1,m2) = fprintf fd "%s,%s" m1 m2 in
-    output_string "cmd_coqc" p.cmd_coqc;
-    output_string "cmd_make" p.cmd_make;
-    output_string "cmd_coqmakefile" p.cmd_coqmakefile;
-    output_string "cmd_coqdoc" p.cmd_coqdoc;
-    output_string "cmd_print" p.cmd_print;
-    
-    output_bool "global_auto_revert" p.global_auto_revert;
-    output_int "global_auto_revert_delay" p.global_auto_revert_delay;
-
-    output_bool "auto_save" p.auto_save;
-    output_int "auto_save_delay" p.auto_save_delay;
-    output_string "auto_save_prefix" (fst p.auto_save_name);
-    output_string "auto_save_suffix" (snd p.auto_save_name);
-
-    output_string "cmd_browse_prefix" (fst p.cmd_browse);
-    output_string "cmd_browse_suffix" (snd p.cmd_browse);
-
-    output_string "doc_url" p.doc_url;
-    output_string "library_url" p.library_url;
-    output_list 
-      "modifier_for_navigation" 
-      output_modi 
-      p.modifier_for_navigation;
-    output_list 
-      "modifier_for_templates" 
-      output_modi 
-      p.modifier_for_templates;
-    output_list 
-      "modifier_for_tactics" 
-      output_modi 
-      p.modifier_for_navigation;
-   output_list 
-      "modifiers_valid" 
-      output_modi 
-      p.modifiers_valid;
-   output_list 
-     "automatic_tactics" 
-     output_tactics
-     p.automatic_tactics;
-*)
-    close_out fd
-
+    let add = Stringmap.add in
+    let (++) x f = f x in
+    Stringmap.empty ++
+    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 "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 "automatic_tactics" 
+      (List.fold_left (fun l (v1,v2) -> v1::v2::l) [] p.automatic_tactics) ++
+    add "cmd_print" [p.cmd_print] ++
+    add "modifier_for_navigation" 
+      (List.map mod_to_str p.modifier_for_navigation) ++
+    add "modifier_for_templates" 
+      (List.map mod_to_str p.modifier_for_templates) ++
+    add "modifier_for_tactics" 
+      (List.map mod_to_str p.modifier_for_tactics) ++
+    add "modifiers_valid" 
+      (List.map mod_to_str p.modifiers_valid) ++
+    add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++
+    add "doc_url" [p.doc_url] ++
+    add "library_url" [p.library_url] ++
+    Config_lexer.print_file pref_file
   with _ -> prerr_endline "Could not save preferences."
   
 let (current:pref ref) = 
@@ -163,58 +137,44 @@ let (current:pref ref) =
 
 let load_pref p = 
   try 
-(*    let l = Config_lexer.get_config pref_file in
-    List.iter 
-      (function k,v -> try match k with
-	 | "cmd_coqc" -> p.cmd_coqc <- v
-	 | "cmd_make" -> p.cmd_make <-  v
-	 | "cmd_coqmakefile" -> p.cmd_coqmakefile <- v
-	 | "cmd_coqdoc" -> p.cmd_coqdoc <-  v
-	 | "cmd_print" -> p.cmd_print <-  v
-	 | "global_auto_revert" -> p.global_auto_revert <- bool_of_string v
-	 | "global_auto_revert_delay" -> 
-	     p.global_auto_revert_delay <- int_of_string v
-	 | "auto_save" -> p.auto_save <- bool_of_string v
-	 | "auto_save_delay" -> p.auto_save_delay <- int_of_string v
-	 | "auto_save_prefix" -> 
-	     let x,y = p.auto_save_name in
-	     p.auto_save_name <- (v,y)
-	 | "auto_save_suffix" -> 
-	     let x,y = p.auto_save_name in
-	     p.auto_save_name <- (x,v)
-	       
-	 | "cmd_browse_prefix" -> 
-	     let x,y = p.cmd_browse in
-	     p.cmd_browse <- (v,y)
-	 | "cmd_browse_suffix" ->
-	     let x,y = p.cmd_browse in
-	     p.cmd_browse <- (x,v)
-	 | "doc_url" -> p.doc_url <- v
-	 | "library_url" -> p.library_url <- v
-	 | "modifier_for_navigation" ->
-	     p.modifier_for_navigation <- 
-	     List.rev_map str_to_mod (Config_lexer.split v)
-	 | "modifier_for_templates" ->
-	     p.modifier_for_templates <- 
-	     List.rev_map str_to_mod (Config_lexer.split v)
-	 | "modifier_for_tactics" ->
-	     p.modifier_for_tactics <- 
-	     List.rev_map str_to_mod (Config_lexer.split v)
-	 | "modifiers_valid" ->
-	     p.modifiers_valid <- 
-	     List.rev_map str_to_mod (Config_lexer.split v)
-	 | "automatic_tactics" ->
-	     p.automatic_tactics <- 
-	     List.map (fun x -> Pervasives.prerr_endline x;(x,"")) (Config_lexer.split v)
-	 | _ -> prerr_endline ("Warning: unknown option "^k)
-       with _ -> ())
-      l
-*)
-    let cin = open_in pref_file in
-    let (new_pref:pref) = input_value cin in
-    close_in cin;
-    current := new_pref
-  with _ -> prerr_endline "Could not load preferences."
+    let m = Config_lexer.load_file pref_file in
+    let np = { !p with cmd_coqc = !p.cmd_coqc } in
+    let set k f = try let v = Stringmap.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
+    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_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 "automatic_tactics"
+      (fun v -> 
+	 let rec from_list = function
+	   | [] | [_] -> []
+	   | x :: y :: l -> (x,y) :: from_list l 
+	 in
+	 np.automatic_tactics <- from_list v);
+    set_hd "cmd_print" (fun v -> np.cmd_print <- v);
+    set "modifier_for_navigation" 
+      (fun v -> np.modifier_for_navigation <- List.map str_to_mod v);
+    set "modifier_for_templates" 
+      (fun v -> np.modifier_for_templates <- List.map str_to_mod v);
+    set "modifier_for_tactics" 
+      (fun v -> np.modifier_for_tactics <- List.map str_to_mod v);
+    set "modifiers_valid" 
+      (fun v -> np.modifiers_valid <- List.map str_to_mod v);
+    set_pair "cmd_browse" (fun v1 v2 -> np.cmd_browse <- (v1,v2));
+    set_hd "doc_url" (fun v -> np.doc_url <- v);
+    set_hd "library_url" (fun v -> np.library_url <- v);
+    current := np
+  with e -> prerr_endline (Printexc.to_string e); prerr_endline "Could not load preferences."
 
 let configure () = 
   let cmd_coqc =