X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fhxp%2FhxpLexer.mll;fp=helm%2Fhxp%2FhxpLexer.mll;h=0000000000000000000000000000000000000000;hp=fbec4aca78b5bc87bece211f959f165bf42d0f6f;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/hxp/hxpLexer.mll b/helm/hxp/hxpLexer.mll deleted file mode 100644 index fbec4aca7..000000000 --- a/helm/hxp/hxpLexer.mll +++ /dev/null @@ -1,56 +0,0 @@ -(* 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://www.cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -{ - open HxpParser -} - -let SPC = [' ' '\t' '\n' '\r' '?' '!']+ -let ALPHA = ['A'-'Z' 'a'-'z']+ -let STR = '"'[^'"']*'"' -let NUM = ['0'-'9' '.']+ -let BEF = [^ '=' '0'-'9' '.' ':' '*']* - -rule xml_token = parse - | SPC { xml_token lexbuf } - | '<' { OPEN } - | '>' { CLOSE } - | '=' { EQ } - | '/' { SL } - | ALPHA { NAME (Lexing.lexeme lexbuf) } - | STR { VAL (Lexing.lexeme lexbuf) } - | eof { DONE } - -and time_token = parse - | BEF { time_token lexbuf } - | NUM { DATA (float_of_string (Lexing.lexeme lexbuf)) } - | '=' { EQ } - | ':' { CLN } - | _ { DONE } - | eof { DONE } -