aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/config_lexer.mll
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-01 09:51:03 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-01 09:51:03 +0000
commit0034b83ed1fa97e106b222dfbaf4df126158cf6d (patch)
treecf3cb065774294863046848e0e1013628fd012cd /ide/config_lexer.mll
parent1ba4c045833569b30fd61616aae739ecb7117ab8 (diff)
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
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r--ide/config_lexer.mll31
1 files changed, 16 insertions, 15 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