blob: 778a9c7e7692dc9305790b5c6764bb8fd263fd10 (
plain)
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
{
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
}
|
