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