X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhxp%2FhxpXML.ml;fp=helm%2Fhxp%2FhxpXML.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=7c4dc4cb473dfe19b64584b27a5e0246d766b20d;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/hxp/hxpXML.ml b/helm/hxp/hxpXML.ml
deleted file mode 100644
index 7c4dc4cb4..000000000
--- a/helm/hxp/hxpXML.ml
+++ /dev/null
@@ -1,91 +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 <fguidi@cs.unibo.it>
- *)
-
-module T = HxpTypes
-
-module type Type = sig
-
-   type handle
-   
-   val start     : string -> bool -> handle
-
-   val stop     : handle -> unit 
-
-   val next     : handle -> T.xml_object   
-
-   val xnext    : handle -> handle * T.xml_xobject
-
-   val scan_for : handle -> T.xml_xobject -> handle
-
-end 
-
-module Make : Type = struct 
-
-   module L = HxpLexer
-   
-   module P = HxpParser
-
-   type mode_t = Text of in_channel * Lexing.lexbuf 
-               | GZip of Gzip.in_channel * Lexing.lexbuf
-
-   type handle = {mode : mode_t; level : int}
-               
-   let start s filter =
-      let gread gch s n = Gzip.input gch s 0 n in
-      if filter then    
-         let gch = Gzip.open_in (s ^ ".gz") in 
-         let glb = Lexing.from_function (gread gch) in 
-         {mode = GZip (gch, glb); level = 0}
-      else
-         let ch = open_in s in
-	 let lb = Lexing.from_channel ch in 
-         {mode = Text (ch, lb); level = 0}
-
-   let stop = function
-      | {mode = GZip (gch, _)} -> Gzip.close_in gch
-      | {mode = Text (ch, _)}  -> close_in ch
-
-   let next h =
-      let lexbuf = match h.mode with
-         | GZip (_, glb) -> glb
-	 | Text (_, lb)  -> lb
-      in
-      P.xml L.xml_token lexbuf
-
-   let xnext h =
-      let obj = next h in
-      match obj with
-      | T.XML_Open _  -> {h with level = succ h.level}, (obj, h.level)
-      | T.XML_Close _ -> {h with level = pred h.level}, (obj, pred h.level)
-      | _             -> h, (obj, h.level)
-
-   let rec scan_for h xobj = 
-      let h, curr_xobj = xnext h in
-      if curr_xobj = xobj then h else scan_for h xobj
-
-end