No more parser for reading coqide pref file

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

2 files changed, 16 insertions, 56 deletions

diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 1aaf2b71a..933baa5dc 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -10,7 +10,6 @@
 
   open Lexing
   open Format
-  open Config_parser
   open Minilib
 
   let string_buffer = Buffer.create 1024
@@ -20,21 +19,23 @@
 let space = [' ' '\010' '\013' '\009' '\012']
 let char = ['A'-'Z' 'a'-'z' '_' '0'-'9']
 let ident = char+
+let ignore = space | ('#' [^ '\n']*)
 
-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)) }
+rule prefs m = parse
+  |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
+				 prefs (Stringmap.add id conf m) lexbuf }
   | _     { let c = lexeme_start lexbuf in
-	    eprintf ".coqiderc: invalid character (%d)\n@." c;
-	    token lexbuf }
-  | eof   { EOF }
+	      eprintf ".coqiderc: invalid character (%d)\n@." c;
+	      prefs m lexbuf }
+  | eof   { m }
+
+and str_list l = parse
+  | ignore* '"'   { Buffer.reset string_buffer;
+		    Buffer.add_char string_buffer '"';
+		    string lexbuf;
+		    let s = Buffer.contents string_buffer in
+		      str_list ((Scanf.sscanf s "%S" (fun s -> s))::l) lexbuf }
+  |ignore+ { List.rev l}
 
 and string = parse
   | '"'  { Buffer.add_char string_buffer '"' }
@@ -47,7 +48,7 @@ and string = parse
   let load_file f =
     let c = open_in f in
     let lb = from_channel c in
-    let m = Config_parser.prefs token lb in
+    let m = prefs Stringmap.empty lb in
     close_in c;
     m
 
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
deleted file mode 100644
index 4ab6950b7..000000000
--- a/ide/config_parser.mly
+++ /dev/null
@@ -1,41 +0,0 @@
-/************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************/
-
-%{
-
-  open Parsing
-  open Minilib
-
-%}
-
-%token <string> IDENT STRING
-%token EQUAL EOF
-
-%type <(string list) Minilib.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 */      { [] }
-;
-