+++ /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 = TxtParser
-
- let out s = if !O.debug_lexer then L.warn s else ()
-}
-
-let BS = "\\"
-let SPC = [' ' '\t' '\n']+
-let OC = "\\*"
-let CC = "*\\"
-let FIG = ['0'-'9']
-let ALPHA = ['A'-'Z' 'a'-'z' '_']
-let QT = '"'
-let ID = ALPHA+ (ALPHA | FIG)*
-let IX = FIG+
-
-rule block_comment = parse
- | CC { () }
- | OC { block_comment lexbuf; block_comment lexbuf }
- | _ { block_comment lexbuf }
-and qstring = parse
- | QT { "" }
- | SPC { " " ^ qstring lexbuf }
- | BS BS { "\\" ^ qstring lexbuf }
- | BS QT { "\"" ^ qstring lexbuf }
- | _ as c { String.make 1 c ^ qstring lexbuf }
-and token = parse
- | SPC { token lexbuf }
- | OC { block_comment lexbuf; token lexbuf }
- | ID as id { out ("ID " ^ id); P.ID id }
- | IX as ix { out ("IX " ^ ix); P.IX (int_of_string ix) }
- | QT { let s = qstring lexbuf in out ("STR " ^ s); P.STR s }
- | "\\graph" { out "GRAPH"; P.GRAPH }
- | "\\decl" { out "DECL"; P.DECL }
- | "\\ax" { out "AX"; P.AX }
- | "\\def" { out "DEF"; P.DEF }
- | "\\th" { out "TH"; P.TH }
- | "\\generate" { out "GEN"; P.GEN }
- | "\\require" { out "REQ"; P.REQ }
- | "\\open" { out "OPEN"; P.OPEN }
- | "\\close" { out "CLOSE"; P.CLOSE }
- | "\\sorts" { out "SORTS"; P.SORTS }
- | "(" { 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 "FS"; P.FS }
- | ":" { out "CN"; P.CN }
- | "," { out "CM"; P.CM }
- | "=" { out "EQ"; P.EQ }
- | "*" { out "STAR"; P.STAR }
- | "#" { out "HASH"; P.HASH }
- | "+" { out "PLUS"; P.PLUS }
- | "~" { out "TE"; P.TE }
- | "->" { out "WTO"; P.WTO }
- | "=>" { out "STO"; P.STO }
- | eof { out "EOF"; P.EOF }