V_______________________________________________________________ *)
{
+ module KT = String
+
module L = Log
module G = Options
module AP = AutParser
-
- let out s = if !G.debug_lexer then L.warn s else ()
+ let level = 0
+
+IFDEF LEXER THEN
+ let out s = if !G.debug_lexer then L.warn level s else ()
+END
+
+IFDEF QUOTE THEN
(* This turns an Automath identifier into an XML nmtoken *)
let quote id =
- let l = String.length id in
- let rec aux i =
- if i < l then begin
- if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
- aux (succ i)
- end else
- id
+ let map = function
+ | '\''
+ | '`' -> '_';
+ | c -> c
in
- aux 0
+ KT.map map id
+
+END
}
let LC = ['#' '%']
| SPC { token lexbuf }
| LC { line_comment lexbuf; token lexbuf }
| OC { block_comment lexbuf; token lexbuf }
- | "_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";
+ | "_E" { IFDEF LEXER THEN out "E" ELSE () END; AP.E }
+ | "'_E'" { IFDEF LEXER THEN out "E" ELSE () END; AP.E }
+ | "---" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB }
+ | "'eb'" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB }
+ | "EB" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB }
+ | "--" { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT }
+ | "PN" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN }
+ | "'pn'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN }
+ | "PRIM" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN }
+ | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN }
+ | "???" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN }
+ | "PROP" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP }
+ | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP }
+ | "TYPE" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE }
+ | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE }
+ | ID { IFDEF LEXER THEN out "ID" ELSE () END;
let s = Lexing.lexeme lexbuf in
- if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
+IFDEF QUOTE THEN
+ if !G.quote then AP.IDENT (quote s) else AP.IDENT s
+ELSE
+ AP.IDENT s
+END
}
- | ":=" { 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 }
+ | ":=" { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF }
+ | "(" { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP }
+ | ")" { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP }
+ | "[" { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB }
+ | "]" { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB }
+ | "<" { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA }
+ | ">" { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA }
+ | "@" { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT }
+ | "~" { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD }
+ | "\"" { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT }
+ | ":" { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN }
+ | "," { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM }
+ | ";" { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC }
+ | "." { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS }
+ | "+" { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS }
+ | "-" { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS }
+ | "*" { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES }
+ | "=" { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF }
+ | eof { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF }