2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
17 let out s = if debug then L.warn s else ()
21 let SPC = [' ' '\t' '\n']+
25 let ALPHA = ['A'-'Z' 'a'-'z' '_']
27 let ID = ALPHA+ (ALPHA | FIG)*
30 rule block_comment = parse
32 | OC { block_comment lexbuf; block_comment lexbuf }
33 | _ { block_comment lexbuf }
36 | SPC { " " ^ qstring lexbuf }
37 | BS BS { "\\" ^ qstring lexbuf }
38 | BS QT { "\"" ^ qstring lexbuf }
39 | _ { Lexing.lexeme lexbuf ^ qstring lexbuf }
41 | SPC { token lexbuf }
42 | OC { block_comment lexbuf; token lexbuf }
43 | ID { out "ID"; P.ID (Lexing.lexeme lexbuf) }
44 | IX { out "IX"; P.IX (int_of_string (Lexing.lexeme lexbuf)) }
45 | QT { let s = qstring lexbuf in out "STR"; P.STR s }
46 | "\\open" { out "OPEN"; P.OPEN }
47 | "\\close" { out "CLOSE"; P.CLOSE }
48 | "\\global" { out "GLOBAL"; P.GLOBAL }
49 | "(" { out "OP"; P.OP }
50 | ")" { out "CP"; P.CP }
51 | "[" { out "OB"; P.OB }
52 | "]" { out "CB"; P.CB }
53 | "<" { out "OA"; P.OA }
54 | ">" { out "CA"; P.CA }
55 | "." { out "FS"; P.FS }
56 | ":" { out "CN"; P.CN }
57 | "," { out "CM"; P.CM }
58 | "=" { out "EQ"; P.EQ }
59 | "*" { out "STAR"; P.STAR }
60 | "#" { out "HASH"; P.HASH }
61 | "+" { out "PLUS"; P.PLUS }
62 | eof { out "EOF"; P.EOF }