1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 let out s = if debug then print_endline s else ()
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 }
52 | SPC { token lexbuf }
53 | LC { line_comment lexbuf; token lexbuf }
54 | OC { block_comment lexbuf; token lexbuf }
55 | "_E" { out "E"; P.E }
56 | "'_E'" { out "E"; P.E }
57 | "---" { out "EB"; P.EB }
58 | "'eb'" { out "EB"; P.EB }
59 | "EB" { out "EB"; P.EB }
60 | "--" { out "EXIT"; P.EXIT }
61 | "PN" { out "PN"; P.PN }
62 | "'pn'" { out "PN"; P.PN }
63 | "PRIM" { out "PN"; P.PN }
64 | "'prim'" { out "PN"; P.PN }
65 | "???" { out "PN"; P.PN }
66 | "PROP" { out "PROP"; P.PROP }
67 | "'prop'" { out "PROP"; P.PROP }
68 | "TYPE" { out "TYPE"; P.TYPE }
69 | "'type'" { out "TYPE"; P.TYPE }
70 | ID { out "ID"; P.IDENT (Lexing.lexeme lexbuf) }
71 | ":=" { out "DEF"; P.DEF }
72 | "(" { out "OP"; P.OP }
73 | ")" { out "CP"; P.CP }
74 | "[" { out "OB"; P.OB }
75 | "]" { out "CB"; P.CB }
76 | "<" { out "OA"; P.OA }
77 | ">" { out "CA"; P.CA }
78 | "@" { out "AT"; P.AT }
79 | "~" { out "TD"; P.TD }
80 | "\"" { out "QT"; P.QT }
81 | ":" { out "CN"; P.CN }
82 | "," { out "CM"; P.CM }
83 | ";" { out "SC"; P.SC }
84 | "." { out "FS"; P.FS }
85 | "+" { out "PLUS"; P.PLUS }
86 | "-" { out "MINUS"; P.MINUS }
87 | "*" { out "TIMES"; P.TIMES }
88 | "=" { out "DEF"; P.DEF }
89 | eof { out "EOF"; P.EOF }