--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+{
+ module L = Log
+ module O = Options
+ module P = AutParser
+
+ let out s = if !O.debug_lexer then L.warn s else ()
+
+(* 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
+ in
+ aux 0
+}
+
+let LC = ['#' '%']
+let OC = "{"
+let CC = "}"
+let SPC = [' ' '\t' '\n']+
+let NL = "\n"
+let ID = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
+
+rule line_comment = parse
+ | NL { () }
+ | OC { block_comment lexbuf; line_comment lexbuf }
+ | _ { line_comment lexbuf }
+ | eof { () }
+and block_comment = parse
+ | CC { () }
+ | OC { block_comment lexbuf; block_comment lexbuf }
+ | LC { line_comment lexbuf; block_comment lexbuf }
+ | _ { block_comment lexbuf }
+and token = parse
+ | 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 }
+ | ID { out "ID";
+ let s = Lexing.lexeme lexbuf in
+ if !O.unquote then P.IDENT s else P.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 }