aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/config_lexer.mll
blob: 8e04331c1b2e61b273ed0dc77425c53e02c16f9b (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___,, * 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$ *)

{

  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

}