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_______________________________________________________________ *)
19 let out s = if !G.debug_lexer then L.warn level s else ()
21 (* This turns an Automath identifier into an XML nmtoken *)
23 let l = String.length id in
26 if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
37 let SPC = [' ' '\t' '\n']+
39 let ID = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
41 rule line_comment = parse
43 | OC { block_comment lexbuf; line_comment lexbuf }
44 | _ { line_comment lexbuf }
46 and block_comment = parse
48 | OC { block_comment lexbuf; block_comment lexbuf }
49 | LC { line_comment lexbuf; block_comment lexbuf }
50 | _ { block_comment lexbuf }
52 | SPC { token lexbuf }
53 | LC { line_comment lexbuf; token lexbuf }
54 | OC { block_comment lexbuf; token lexbuf }
55 | "_E" { out "E"; AP.E }
56 | "'_E'" { out "E"; AP.E }
57 | "---" { out "EB"; AP.EB }
58 | "'eb'" { out "EB"; AP.EB }
59 | "EB" { out "EB"; AP.EB }
60 | "--" { out "EXIT"; AP.EXIT }
61 | "PN" { out "PN"; AP.PN }
62 | "'pn'" { out "PN"; AP.PN }
63 | "PRIM" { out "PN"; AP.PN }
64 | "'prim'" { out "PN"; AP.PN }
65 | "???" { out "PN"; AP.PN }
66 | "PROP" { out "PROP"; AP.PROP }
67 | "'prop'" { out "PROP"; AP.PROP }
68 | "TYPE" { out "TYPE"; AP.TYPE }
69 | "'type'" { out "TYPE"; AP.TYPE }
71 let s = Lexing.lexeme lexbuf in
72 if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
74 | ":=" { out "DEF"; AP.DEF }
75 | "(" { out "OP"; AP.OP }
76 | ")" { out "CP"; AP.CP }
77 | "[" { out "OB"; AP.OB }
78 | "]" { out "CB"; AP.CB }
79 | "<" { out "OA"; AP.OA }
80 | ">" { out "CA"; AP.CA }
81 | "@" { out "AT"; AP.AT }
82 | "~" { out "TD"; AP.TD }
83 | "\"" { out "QT"; AP.QT }
84 | ":" { out "CN"; AP.CN }
85 | "," { out "CM"; AP.CM }
86 | ";" { out "SC"; AP.SC }
87 | "." { out "FS"; AP.FS }
88 | "+" { out "PLUS"; AP.PLUS }
89 | "-" { out "MINUS"; AP.MINUS }
90 | "*" { out "TIMES"; AP.TIMES }
91 | "=" { out "DEF"; AP.DEF }
92 | eof { out "EOF"; AP.EOF }