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