diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /ide/config_lexer.mll |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r-- | ide/config_lexer.mll | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll new file mode 100644 index 00000000..1c0720d1 --- /dev/null +++ b/ide/config_lexer.mll @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: config_lexer.mll,v 1.4.2.1 2004/07/16 19:30:19 herbelin Exp $ *) + +{ + + open Lexing + open Format + open Config_parser + open Util + + let string_buffer = Buffer.create 1024 + +} + +let space = [' ' '\010' '\013' '\009' '\012'] +let char = ['A'-'Z' 'a'-'z' '_' '0'-'9'] +let ident = char+ + +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 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 + +} |