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 ()
25 let SPC = [' ' '\t' '\n']+
29 let ALPHA = ['A'-'Z' 'a'-'z' '_']
31 let ID = ALPHA+ (ALPHA | FIG)*
34 rule block_comment = parse
36 | OC { block_comment lexbuf; block_comment lexbuf }
37 | _ { block_comment lexbuf }
40 | SPC { " " ^ qstring lexbuf }
41 | BS BS { "\\" ^ qstring lexbuf }
42 | BS QT { "\"" ^ qstring lexbuf }
43 | _ as c { String.make 1 c ^ qstring lexbuf }
45 | SPC { token lexbuf }
46 | OC { block_comment lexbuf; token lexbuf }
47 | ID as id { IFDEF LEXER THEN out ("ID " ^ id) ELSE () END; TP.ID id }
48 | IX as ix { IFDEF LEXER THEN out ("IX " ^ ix) ELSE () END; TP.IX (int_of_string ix) }
49 | QT { let s = qstring lexbuf in
50 IFDEF LEXER THEN out ("STR " ^ s) ELSE () END; TP.STR s
52 | "\\graph" { IFDEF LEXER THEN out "GRAPH" ELSE () END; TP.GRAPH }
53 | "\\main" { IFDEF LEXER THEN out "MAIN" ELSE () END; TP.MAIN }
54 | "\\decl" { IFDEF LEXER THEN out "DECL" ELSE () END; TP.DECL }
55 | "\\ax" { IFDEF LEXER THEN out "AX" ELSE () END; TP.AX }
56 | "\\cong" { IFDEF LEXER THEN out "CONG" ELSE () END; TP.CONG }
57 | "\\def" { IFDEF LEXER THEN out "DEF" ELSE () END; TP.DEF }
58 | "\\th" { IFDEF LEXER THEN out "TH" ELSE () END; TP.TH }
59 | "\\generate" { IFDEF LEXER THEN out "GEN" ELSE () END; TP.GEN }
60 | "\\require" { IFDEF LEXER THEN out "REQ" ELSE () END; TP.REQ }
61 | "\\open" { IFDEF LEXER THEN out "OPEN" ELSE () END; TP.OPEN }
62 | "\\close" { IFDEF LEXER THEN out "CLOSE" ELSE () END; TP.CLOSE }
63 | "\\sorts" { IFDEF LEXER THEN out "SORTS" ELSE () END; TP.SORTS }
64 | "(" { IFDEF LEXER THEN out "OP" ELSE () END; TP.OP }
65 | ")" { IFDEF LEXER THEN out "CP" ELSE () END; TP.CP }
66 | "[" { IFDEF LEXER THEN out "OB" ELSE () END; TP.OB }
67 | "]" { IFDEF LEXER THEN out "CB" ELSE () END; TP.CB }
68 | "{" { IFDEF LEXER THEN out "OC" ELSE () END; TP.OC }
69 | "}" { IFDEF LEXER THEN out "CC" ELSE () END; TP.CC }
70 | "<" { IFDEF LEXER THEN out "OA" ELSE () END; TP.OA }
71 | ">" { IFDEF LEXER THEN out "CA" ELSE () END; TP.CA }
72 | "." { IFDEF LEXER THEN out "FS" ELSE () END; TP.FS }
73 | ":" { IFDEF LEXER THEN out "CN" ELSE () END; TP.CN }
74 | "," { IFDEF LEXER THEN out "CM" ELSE () END; TP.CM }
75 | "=" { IFDEF LEXER THEN out "EQ" ELSE () END; TP.EQ }
76 | "*" { IFDEF LEXER THEN out "STAR" ELSE () END; TP.STAR }
77 | "#" { IFDEF LEXER THEN out "HASH" ELSE () END; TP.HASH }
78 | "~" { IFDEF LEXER THEN out "TE" ELSE () END; TP.TE }
79 | "^" { IFDEF LEXER THEN out "CT" ELSE () END; TP.CT }
80 | eof { IFDEF LEXER THEN out "EOF" ELSE () END; TP.EOF }