(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

{ 
   module P = AutParser
   
   let debug = false
   let out s = if debug then print_endline s else ()
}

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 }
   | eof { () } 
and token = parse
   | SPC      { token lexbuf } 
   | LC       { line_comment lexbuf; token lexbuf  }
   | OC       { block_comment lexbuf; token lexbuf }
   | "_E"     { out "E"; P.E         }
   | "'_E'"   { out "E"; P.E         }
   | "---"    { out "EB"; P.EB       }
   | "'eb'"   { out "EB"; P.EB       }
   | "EB"     { out "EB"; P.EB       }
   | "--"     { out "EXIT"; P.EXIT   }
   | "PN"     { out "PN"; P.PN       }
   | "'pn'"   { out "PN"; P.PN       }
   | "PRIM"   { out "PN"; P.PN       }
   | "'prim'" { out "PN"; P.PN       }
   | "???"    { out "PN"; P.PN       }
   | "PROP"   { out "PROP"; P.PROP   }
   | "'prop'" { out "PROP"; P.PROP   }
   | "TYPE"   { out "TYPE"; P.TYPE   }
   | "'type'" { out "TYPE"; P.TYPE   }
   | ID       { out "ID"; P.IDENT (Lexing.lexeme lexbuf) }   
   | ":="     { out "DEF"; P.DEF     }
   | "("      { 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 "AT"; P.AT       }
   | "~"      { out "TD"; P.TD       }
   | "\""     { out "QT"; P.QT       }
   | ":"      { out "CN"; P.CN       }   
   | ","      { out "CM"; P.CM       }
   | ";"      { out "SC"; P.SC       }
   | "."      { out "FS"; P.FS       }   
   | "+"      { out "PLUS"; P.PLUS   }
   | "-"      { out "MINUS"; P.MINUS }
   | "*"      { out "TIMES"; P.TIMES }
   | "="      { out "DEF"; P.DEF     }
   | eof      { out "EOF"; P.EOF     }