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