(*
    ||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 P = TxtParser
   
   let debug = false
   let out s = if debug 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                 } 
   | _     { Lexing.lexeme lexbuf ^ qstring lexbuf }
and token = parse
   | SPC       { token lexbuf                                 } 
   | OC        { block_comment lexbuf; token lexbuf           }
   | ID as id  { out "ID"; P.ID id                            }
   | IX as ix  { out "IX"; P.IX (int_of_string ix)            }
   | QT        { let s = qstring lexbuf in out "STR"; 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       }
   | "\\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     }