(*
    ||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 G  = Options
   module TP = TxtParser

   let level = 0

IFDEF LEXER THEN   
   let out s = if !G.debug_lexer then L.warn level s else ()
END
}

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     { IFDEF LEXER THEN out ("ID " ^ id) ELSE () END; TP.ID id                 }
   | IX as ix     { IFDEF LEXER THEN out ("IX " ^ ix) ELSE () END; TP.IX (int_of_string ix) }
   | QT           { let s = qstring lexbuf in
                    IFDEF LEXER THEN out ("STR " ^ s) ELSE () END; TP.STR s
                  }
   | "\\graph"    { IFDEF LEXER THEN out "GRAPH" ELSE () END; TP.GRAPH }
   | "\\main"     { IFDEF LEXER THEN out "MAIN" ELSE () END; TP.MAIN   }
   | "\\decl"     { IFDEF LEXER THEN out "DECL" ELSE () END; TP.DECL   }
   | "\\ax"       { IFDEF LEXER THEN out "AX" ELSE () END; TP.AX       }
   | "\\cong"     { IFDEF LEXER THEN out "CONG" ELSE () END; TP.CONG   }
   | "\\def"      { IFDEF LEXER THEN out "DEF" ELSE () END; TP.DEF     }
   | "\\th"       { IFDEF LEXER THEN out "TH" ELSE () END; TP.TH       }
   | "\\generate" { IFDEF LEXER THEN out "GEN" ELSE () END; TP.GEN     }
   | "\\require"  { IFDEF LEXER THEN out "REQ" ELSE () END; TP.REQ     }
   | "\\open"     { IFDEF LEXER THEN out "OPEN" ELSE () END; TP.OPEN   } 
   | "\\close"    { IFDEF LEXER THEN out "CLOSE" ELSE () END; TP.CLOSE }
   | "\\sorts"    { IFDEF LEXER THEN out "SORTS" ELSE () END; TP.SORTS }
   | "("          { IFDEF LEXER THEN out "OP" ELSE () END; TP.OP       }
   | ")"          { IFDEF LEXER THEN out "CP" ELSE () END; TP.CP       }
   | "["          { IFDEF LEXER THEN out "OB" ELSE () END; TP.OB       }
   | "]"          { IFDEF LEXER THEN out "CB" ELSE () END; TP.CB       }
   | "{"          { IFDEF LEXER THEN out "OC" ELSE () END; TP.OC       }
   | "}"          { IFDEF LEXER THEN out "CC" ELSE () END; TP.CC       }
   | "<"          { IFDEF LEXER THEN out "OA" ELSE () END; TP.OA       }
   | ">"          { IFDEF LEXER THEN out "CA" ELSE () END; TP.CA       }
   | "."          { IFDEF LEXER THEN out "FS" ELSE () END; TP.FS       }   
   | ":"          { IFDEF LEXER THEN out "CN" ELSE () END; TP.CN       }   
   | ","          { IFDEF LEXER THEN out "CM" ELSE () END; TP.CM       }
   | "="          { IFDEF LEXER THEN out "EQ" ELSE () END; TP.EQ       }
   | "*"          { IFDEF LEXER THEN out "STAR" ELSE () END; TP.STAR   }
   | "#"          { IFDEF LEXER THEN out "HASH" ELSE () END; TP.HASH   }
   | "~"          { IFDEF LEXER THEN out "TE" ELSE () END; TP.TE       }
   | "^"          { IFDEF LEXER THEN out "CT" ELSE () END; TP.CT       }
   | eof          { IFDEF LEXER THEN out "EOF" ELSE () END; TP.EOF     }