1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
{
open Lexing
open Format
let string_buffer = Buffer.create 1024
}
let space = [' ' '\010' '\013' '\009' '\012']
let char = ['A'-'Z' 'a'-'z' '_' '0'-'9']
let ident = (char | '.')+
let ignore = space | ('#' [^ '\n']*)
rule prefs m = parse
|ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
prefs (Util.String.Map.add id conf m) lexbuf }
| _ { let c = lexeme_start lexbuf in
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 '"' }
| '\\' '"' | _
{ 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 = prefs Util.String.Map.empty 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
Util.String.Map.iter
(fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
fprintf fmt "@.";
close_out c
}
|