V_______________________________________________________________ *)
{
- module L = Log
- module O = Options
- module P = AutParser
+ module L = Log
+ module G = Options
+ module AP = AutParser
- let out s = if !O.debug_lexer then L.warn s else ()
+ let out s = if !G.debug_lexer then L.warn s else ()
(* This turns an Automath identifier into an XML nmtoken *)
let quote id =
| SPC { token lexbuf }
| LC { line_comment lexbuf; token lexbuf }
| OC { block_comment lexbuf; token lexbuf }
- | "_E" { out "E"; P.E }
- | "'_E'" { out "E"; P.E }
- | "---" { out "EB"; P.EB }
- | "'eb'" { out "EB"; P.EB }
- | "EB" { out "EB"; P.EB }
- | "--" { out "EXIT"; P.EXIT }
- | "PN" { out "PN"; P.PN }
- | "'pn'" { out "PN"; P.PN }
- | "PRIM" { out "PN"; P.PN }
- | "'prim'" { out "PN"; P.PN }
- | "???" { out "PN"; P.PN }
- | "PROP" { out "PROP"; P.PROP }
- | "'prop'" { out "PROP"; P.PROP }
- | "TYPE" { out "TYPE"; P.TYPE }
- | "'type'" { out "TYPE"; P.TYPE }
+ | "_E" { out "E"; AP.E }
+ | "'_E'" { out "E"; AP.E }
+ | "---" { out "EB"; AP.EB }
+ | "'eb'" { out "EB"; AP.EB }
+ | "EB" { out "EB"; AP.EB }
+ | "--" { out "EXIT"; AP.EXIT }
+ | "PN" { out "PN"; AP.PN }
+ | "'pn'" { out "PN"; AP.PN }
+ | "PRIM" { out "PN"; AP.PN }
+ | "'prim'" { out "PN"; AP.PN }
+ | "???" { out "PN"; AP.PN }
+ | "PROP" { out "PROP"; AP.PROP }
+ | "'prop'" { out "PROP"; AP.PROP }
+ | "TYPE" { out "TYPE"; AP.TYPE }
+ | "'type'" { out "TYPE"; AP.TYPE }
| ID { out "ID";
let s = Lexing.lexeme lexbuf in
- if !O.unquote then P.IDENT s else P.IDENT (quote s)
+ if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
}
- | ":=" { out "DEF"; P.DEF }
- | "(" { out "OP"; P.OP }
- | ")" { out "CP"; P.CP }
- | "[" { out "OB"; P.OB }
- | "]" { out "CB"; P.CB }
- | "<" { out "OA"; P.OA }
- | ">" { out "CA"; P.CA }
- | "@" { out "AT"; P.AT }
- | "~" { out "TD"; P.TD }
- | "\"" { out "QT"; P.QT }
- | ":" { out "CN"; P.CN }
- | "," { out "CM"; P.CM }
- | ";" { out "SC"; P.SC }
- | "." { out "FS"; P.FS }
- | "+" { out "PLUS"; P.PLUS }
- | "-" { out "MINUS"; P.MINUS }
- | "*" { out "TIMES"; P.TIMES }
- | "=" { out "DEF"; P.DEF }
- | eof { out "EOF"; P.EOF }
+ | ":=" { out "DEF"; AP.DEF }
+ | "(" { out "OP"; AP.OP }
+ | ")" { out "CP"; AP.CP }
+ | "[" { out "OB"; AP.OB }
+ | "]" { out "CB"; AP.CB }
+ | "<" { out "OA"; AP.OA }
+ | ">" { out "CA"; AP.CA }
+ | "@" { out "AT"; AP.AT }
+ | "~" { out "TD"; AP.TD }
+ | "\"" { out "QT"; AP.QT }
+ | ":" { out "CN"; AP.CN }
+ | "," { out "CM"; AP.CM }
+ | ";" { out "SC"; AP.SC }
+ | "." { out "FS"; AP.FS }
+ | "+" { out "PLUS"; AP.PLUS }
+ | "-" { out "MINUS"; AP.MINUS }
+ | "*" { out "TIMES"; AP.TIMES }
+ | "=" { out "DEF"; AP.DEF }
+ | eof { out "EOF"; AP.EOF }