File: config_lexer.mll

package info (click to toggle)
coq-doc 8.2pl1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: squeeze
  • size: 19,240 kB
  • ctags: 22,737
  • sloc: ml: 132,933; ansic: 1,960; sh: 1,366; lisp: 456; makefile: 327
file content (68 lines) | stat: -rw-r--r-- 1,998 bytes parent folder | download | duplicates (3)
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: config_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *)

{

  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

}