(*
    ||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 KT = String

   module L  = Log
   module G  = Options
   module AP = AutParser

   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 map = function
         | '\''
         | '`' -> '_';
         | c   -> c
      in
      KT.map map id

END
}

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"     { 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
IFDEF QUOTE THEN
                   if !G.quote then AP.IDENT (quote s) else AP.IDENT s
ELSE
                   AP.IDENT s
END
              }
   | ":="     { 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     }