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