+++ /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 }