]> matita.cs.unibo.it Git - helm.git/commitdiff
New implementation that uses the new HELM OCaml libraries.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 27 Nov 2001 13:12:34 +0000 (13:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 27 Nov 2001 13:12:34 +0000 (13:12 +0000)
18 files changed:
helm/metadata/create2/touch/Makefile
helm/metadata/create2/touch/cic.ml [deleted file]
helm/metadata/create2/touch/cicParser.ml [deleted file]
helm/metadata/create2/touch/cicParser.mli [deleted file]
helm/metadata/create2/touch/cicParser2.ml [deleted file]
helm/metadata/create2/touch/cicParser2.mli [deleted file]
helm/metadata/create2/touch/cicParser3.ml [deleted file]
helm/metadata/create2/touch/cicParser3.mli [deleted file]
helm/metadata/create2/touch/clientHTTP.ml [deleted file]
helm/metadata/create2/touch/clientHTTP.mli [deleted file]
helm/metadata/create2/touch/configuration.ml.in [deleted file]
helm/metadata/create2/touch/csc_pxp_reader.ml [deleted file]
helm/metadata/create2/touch/deannotate.ml [deleted file]
helm/metadata/create2/touch/getter.ml [deleted file]
helm/metadata/create2/touch/getter.mli [deleted file]
helm/metadata/create2/touch/pxpUriResolver.ml [deleted file]
helm/metadata/create2/touch/uriManager.ml [deleted file]
helm/metadata/create2/touch/uriManager.mli [deleted file]

index 2d7ef5a8a3e17b63762cd56eea3a38bf6088922f..5296fa723a0643c9d313c35b3635bc2485920d5f 100644 (file)
@@ -1,5 +1,6 @@
-OCAMLOPTIONS = -package netstring -package netclient -package pxp
-
+REQUIRES = helm-getter helm-cic str
+PREDICATES =
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
 OCAMLDEP = ocamldep
 OCAMLFIND = ocamlfind
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS)
@@ -8,18 +9,9 @@ OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
 all: touch
 opt: touch.opt
 
-DEPOBJS = csc_pxp_reader.ml configuration.ml \
-          clientHTTP.ml clientHTTP.mli cic.ml deannotate.ml \
-          uriManager.ml uriManager.mli getter.ml getter.mli \
-          pxpUriResolver.ml cicParser3.ml cicParser3.mli \
-          cicParser2.ml cicParser2.mli cicParser.ml \
-          cicParser.mli touch.ml
-
-TOUCHOBJS = csc_pxp_reader.cmo configuration.cmo \
-            clientHTTP.cmo cic.cmo deannotate.cmo \
-            uriManager.cmo getter.cmo pxpUriResolver.ml \
-            cicParser3.cmo cicParser2.cmo cicParser.cmo \
-            touch.cmo
+DEPOBJS = touch.ml
+
+TOUCHOBJS = touch.cmo
 
 depend:
        $(OCAMLDEP) $(DEPOBJS) > .depend
diff --git a/helm/metadata/create2/touch/cic.ml b/helm/metadata/create2/touch/cic.ml
deleted file mode 100644 (file)
index 8c08b00..0000000
+++ /dev/null
@@ -1,162 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 14/06/2000                                 *)
-(*                                                                            *)
-(* This module defines the internal representation of the objects (variables, *)
-(* blocks of (co)inductive definitions and constants) and the terms of cic    *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* STUFF TO MANAGE IDENTIFIERS *)
-type id = string  (* the abstract type of the (annotated) node identifiers *)
-type anntarget =
-   Object of annobj
- | Term of annterm
-
-(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
-and sort =
-   Prop
- | Set
- | Type
-and name =
-   Name of string
- | Anonimous
-and term =
-   Rel of int                                       (* DeBrujin index *)
- | Var of UriManager.uri                            (* uri *)
- | Meta of int                                      (* numeric id *)
- | Sort of sort                                     (* sort *)
- | Implicit                                         (* *)
- | Cast of term * term                              (* value, type *)
- | Prod of name * term * term                       (* binder, source, target *)
- | Lambda of name * term * term                     (* binder, source, target *)
- | LetIn of name * term * term                      (* binder, term, target *)
- | Appl of term list                                (* arguments *)
- | Const of UriManager.uri * int                    (* uri, number of cookings*)
- | Abst of UriManager.uri                           (* uri *)
- | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
- | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
-    int * int                                       (*  typeno, consno  *)
- (*CSC: serve cookingsno?*)
- | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
-    int *                                           (*  ind. typeno,         *)
-    term * term *                                   (*  outtype, ind. term   *)
-    term list                                       (*  patterns             *)
- | Fix of int * inductiveFun list                   (* funno, functions *)
- | CoFix of int * coInductiveFun list               (* funno, functions *)
-and obj =
-   Definition of string * term * term *           (* id, value, type,         *)
-    (int * UriManager.uri list) list              (*  parameters              *)
- | Axiom of string * term *
-    (int * UriManager.uri list) list              (* id, type, parameters     *)
- | Variable of string * term option * term        (* name, body, type         *)
- | CurrentProof of string * (int * term) list *   (* name, conjectures,       *)
-    term * term                                   (*  value, type             *)
- | InductiveDefinition of inductiveType list *    (* inductive types,         *)
-    (int * UriManager.uri list) list * int        (*  parameters, n ind. pars *)
-and inductiveType = 
- string * bool * term *                       (* typename, inductive, arity *)
-  constructor list                            (*  constructors              *)
-and constructor =
- string * term * bool list option ref         (* id, type, really recursive *)
-and inductiveFun =
- string * int * term * term                   (* name, ind. index, type, body *)
-and coInductiveFun =
- string * term * term                         (* name, type, body *)
-
-and annterm =
-   ARel of id * annotation option ref *
-    int * string option                             (* DeBrujin index, binder *)
- | AVar of id * annotation option ref *             
-    UriManager.uri                                  (* uri *)
- | AMeta of id * annotation option ref * int        (* numeric id *)
- | ASort of id * annotation option ref * sort       (* sort *)
- | AImplicit of id * annotation option ref          (* *)
- | ACast of id * annotation option ref *
-    annterm * annterm                               (* value, type *)
- | AProd of id * annotation option ref *
-    name * annterm * annterm                        (* binder, source, target *)
- | ALambda of id * annotation option ref *
-    name * annterm * annterm                        (* binder, source, target *)
- | ALetIn of id * annotation option ref *
-    name * annterm * annterm                        (* binder, term, target *)
- | AAppl of id * annotation option ref *
-    annterm list                                    (* arguments *)
- | AConst of id * annotation option ref *
-    UriManager.uri * int                            (* uri, number of cookings*)
- | AAbst of id * annotation option ref *
-    UriManager.uri                                  (* uri *)
- | AMutInd of id * annotation option ref *
-    UriManager.uri * int * int                      (* uri, cookingsno, typeno*)
- | AMutConstruct of id * annotation option ref *
-    UriManager.uri * int *                          (* uri, cookingsno, *)
-    int * int                                       (*  typeno, consno  *)
- (*CSC: serve cookingsno?*)
- | AMutCase of id * annotation option ref *
-    UriManager.uri * int *                          (* ind. uri, cookingsno  *)
-    int *                                           (*  ind. typeno,         *)
-    annterm * annterm *                             (*  outtype, ind. term   *)
-    annterm list                                    (*  patterns             *)
- | AFix of id * annotation option ref *
-    int * anninductiveFun list                      (* funno, functions *)
- | ACoFix of id * annotation option ref *
-    int * anncoInductiveFun list                    (* funno, functions *)
-and annobj =
-   ADefinition of id * annotation option ref *
-    string *                                        (* id,           *)
-    annterm * annterm *                             (*  value, type, *)
-    (int * UriManager.uri list) list exactness      (*  parameters   *)
- | AAxiom of id * annotation option ref *
-    string * annterm *                              (* id, type    *)
-    (int * UriManager.uri list) list                (*  parameters *)
- | AVariable of id * annotation option ref *
-    string * annterm option * annterm               (* name, body, type *)
- | ACurrentProof of id * annotation option ref *
-    string * (int * annterm) list *                 (*  name, conjectures, *)
-    annterm * annterm                               (*  value, type        *)
- | AInductiveDefinition of id *
-    annotation option ref * anninductiveType list * (* inductive types ,      *)
-    (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
-and anninductiveType = 
- string * bool * annterm *                    (* typename, inductive, arity *)
-  annconstructor list                         (*  constructors              *)
-and annconstructor =
- string * annterm * bool list option ref      (* id, type, really recursive *)
-and anninductiveFun =
- string * int * annterm * annterm             (* name, ind. index, type, body *)
-and anncoInductiveFun =
- string * annterm * annterm                   (* name, type, body *)
-and annotation =
- string
-and 'a exactness =
-   Possible of 'a                            (* an approximation to something *)
- | Actual of 'a                              (* something *)
-;;
diff --git a/helm/metadata/create2/touch/cicParser.ml b/helm/metadata/create2/touch/cicParser.ml
deleted file mode 100644 (file)
index bf75243..0000000
+++ /dev/null
@@ -1,95 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This is the main (top level) module of a parser for cic objects from xml   *)
-(* files to the internal representation. It uses the modules cicParser2       *)
-(* (objects level) and cicParser3 (terms level)                               *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception Warnings;;
-
-class warner =
-  object 
-    method warn w =
-      print_endline ("WARNING: " ^ w) ;
-      (raise Warnings : unit)
-  end
-;;
-
-exception EmptyUri;;
-
-(* given an uri u it returns the list of tokens of the base uri of u *)
-(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"]   *)
-let tokens_of_uri uri =
- let uri' = UriManager.string_of_uri uri in
- let rec chop_list =
-  function
-     [] -> raise EmptyUri
-   | he::[fn] -> [he]
-   | he::tl -> he::(chop_list tl)
- in
-  let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in
-   let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in
-    chop_list list_of_tokens
-;;
-
-(* given the filename of an xml file of a cic object it returns its internal *)
-(* representation. process_annotations is true if the annotations do really  *)
-(* matter                                                                    *)
-let term_of_xml filename uri process_annotations =
- let module Y = Pxp_yacc in
-  try 
-    let d =
-      (* sets the current base uri to resolve relative URIs *)
-      CicParser3.current_sp := tokens_of_uri uri ;
-      CicParser3.current_uri := uri ;
-      CicParser3.process_annotations := process_annotations ;
-      CicParser3.ids_to_targets :=
-       if process_annotations then Some (Hashtbl.create 500) else None ;
-      let config = {Y.default_config with Y.warner = new warner} in
-      Y.parse_document_entity config
-(*PXP       (Y.ExtID (Pxp_types.System filename,
-         new Pxp_reader.resolve_as_file ~url_of_id ()))
-*)     (PxpUriResolver.from_file filename)
-       CicParser3.domspec
-    in
-     let ids_to_targets = !CicParser3.ids_to_targets in
-      let res = (CicParser2.get_term d#root, ids_to_targets) in
-       CicParser3.ids_to_targets := None ; (* let's help the GC *)
-       res
-  with
-   e ->
-     print_endline ("Filename: " ^ filename ^ "\nException: ") ;
-     print_endline (Pxp_types.string_of_exn e) ;
-     raise e
-;;
diff --git a/helm/metadata/create2/touch/cicParser.mli b/helm/metadata/create2/touch/cicParser.mli
deleted file mode 100644 (file)
index 0078f6f..0000000
+++ /dev/null
@@ -1,44 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 22/03/2000                                 *)
-(*                                                                            *)
-(* This is the main (top level) module of a parser for cic objects from xml   *)
-(* files to the internal representation. It uses the modules cicParser2       *)
-(* (objects level) and cicParser3 (terms level)                               *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* given the filename of an xml file of a cic object and it's uri, it returns *)
-(* its internal annotated representation. The boolean is set to true if the   *)
-(* annotations do really matter                                               *)
-val term_of_xml :
- string -> UriManager.uri -> bool ->
-  Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option
diff --git a/helm/metadata/create2/touch/cicParser2.ml b/helm/metadata/create2/touch/cicParser2.ml
deleted file mode 100644 (file)
index 562f79b..0000000
+++ /dev/null
@@ -1,289 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it>              *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module is the objects level of a parser for cic objects from xml      *)
-(* files to the internal representation. It uses the module cicParser3        *)
-(* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
-(* level).                                                                    *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception IllFormedXml of int;;
-exception NotImplemented;;
-
-(* Utility functions that transform a Pxp attribute into something useful *)
-
-(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
-(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
-let mk_absolute_uris s =
- let l = (Str.split (Str.regexp ":") s) in
-  let absolute_of_relative n v =
-   let module P3 = CicParser3 in
-    let rec mkburi =
-     function
-        (0,_) -> "/"
-      | (n,he::tl) when n > 0 ->
-         "/" ^ he ^ mkburi (n - 1, tl)
-      | _ -> raise (IllFormedXml 12)
-    in
-     let m = List.length !P3.current_sp - (int_of_string n) in
-      let buri = mkburi (m, !P3.current_sp) in
-       UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
-  in
-   let rec absolutize =
-    function
-       [] -> []
-     | [no ; vs] ->
-        let vars = (Str.split (Str.regexp " ") vs) in
-         [(int_of_string no, List.map (absolute_of_relative no) vars)]
-     | no::vs::tl -> 
-        let vars = (Str.split (Str.regexp " ") vs) in
-         let rec add_prefix =
-          function
-             [no2] -> ([], no2)
-           | he::tl ->
-              let (pvars, no2) = add_prefix tl in
-               ((absolute_of_relative no he)::pvars, no2)
-           | _ -> raise (IllFormedXml 11)
-         in
-          let (pvars, no2) = add_prefix vars in
-           (int_of_string no, pvars)::(absolutize (no2::tl))
-     | _ -> raise (IllFormedXml 10)
-   in
-    (* last parameter must be applied first *)
-    absolutize l
-;;
-
-let option_uri_list_of_attr a1 a2 =
- let module T = Pxp_types in
-  let parameters =
-   match a1 with
-      T.Value s -> mk_absolute_uris s
-    | _ -> raise (IllFormedXml 0)
-  in
-   match a2 with
-      T.Value "POSSIBLE" -> Cic.Possible parameters
-    | T.Implied_value -> Cic.Actual parameters
-    | _ -> raise (IllFormedXml 0)
-;;
-
-let uri_list_of_attr a =
- let module T = Pxp_types in
-  match a with
-     T.Value s -> mk_absolute_uris s
-   | _ -> raise (IllFormedXml 0)
-;;
-
-let string_of_attr a =
- let module T = Pxp_types in
-  match a with
-     T.Value s -> s
-   | _ -> raise (IllFormedXml 0)
-;;
-
-let int_of_attr a =
- int_of_string (string_of_attr a)
-;;
-
-let bool_of_attr a =
- bool_of_string (string_of_attr a)
-;;
-
-(* Other utility functions *)
-
-let get_content n =
- match n#sub_nodes with
-    [ t ] -> t
-  | _     -> raise (IllFormedXml 1)
-;;
-
-let register_id id node =
- if !CicParser3.process_annotations then
-  match !CicParser3.ids_to_targets with
-     None -> assert false
-   | Some ids_to_targets ->
-      Hashtbl.add ids_to_targets id (Cic.Object node)
-;;
-
-(* Functions that, given the list of sons of a node of the cic dom (objects   *)
-(* level), retrieve the internal representation associated to the node.       *)
-(* Everytime a cic term subtree is found, it is translated to the internal    *)
-(* representation using the method to_cic_term defined in cicParser3.         *)
-(* Each function raise IllFormedXml if something goes wrong, but this should  *)
-(* be impossible due to the presence of the dtd                               *)
-(* The functions should really be obvious looking at their name and the cic   *)
-(* dtd                                                                        *)
-
-(* called when a CurrentProof is found *)
-let get_conjs_value_type l =
- let rec rget (c, v, t) l =
-  let module D = Pxp_document in
-   match l with
-      [] -> (c, v, t)
-    | conj::tl when conj#node_type = D.T_element "Conjecture" ->
-       let no = int_of_attr (conj#attribute "no")
-       and typ = (get_content conj)#extension#to_cic_term in
-        rget ((no, typ)::c, v, t) tl
-    | value::tl when value#node_type = D.T_element "body" ->
-       let v' = (get_content value)#extension#to_cic_term in
-        (match v with
-            None -> rget (c, Some v', t) tl
-          | _    -> raise (IllFormedXml 2)
-        )
-    | typ::tl when typ#node_type = D.T_element "type" ->
-       let t' = (get_content typ)#extension#to_cic_term in
-        (match t with
-            None -> rget (c, v, Some t') tl
-          | _    -> raise (IllFormedXml 3)
-        )
-    | _ -> raise (IllFormedXml 4)
- in
-  match rget ([], None, None) l with
-     (c, Some v, Some t) -> (c, v, t)
-   | _ -> raise (IllFormedXml 5)
-;;
-
-(* used only by get_inductive_types; called one time for each inductive  *)
-(* definitions in a block of inductive definitions                       *)
-let get_names_arity_constructors l =
- let rec rget (a,c) l =
-  let module D = Pxp_document in
-   match l with
-      [] -> (a, c)
-    | arity::tl when arity#node_type = D.T_element "arity" ->
-       let a' = (get_content arity)#extension#to_cic_term in
-        rget (Some a',c) tl
-    | con::tl when con#node_type = D.T_element "Constructor" ->
-       let id = string_of_attr (con#attribute "name")
-       and ty = (get_content con)#extension#to_cic_term in
-         rget (a,(id,ty,ref None)::c) tl
-    | _ -> raise (IllFormedXml 9)
- in
-  match rget (None,[]) l with
-     (Some a, c) -> (a, List.rev c)
-   | _ -> raise (IllFormedXml 8)
-;;
-
-(* called when an InductiveDefinition is found *)
-let rec get_inductive_types =
- function
-    []     -> []
-  | he::tl ->
-     let tyname    = string_of_attr (he#attribute "name")
-     and inductive = bool_of_attr   (he#attribute "inductive")
-     and (arity,cons) =
-      get_names_arity_constructors (he#sub_nodes)
-     in
-      (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
-;;
-
-(* This is the main function and also the only one used directly from *)
-(* cicParser. Given the root of the dom tree, it returns the internal *)
-(* representation of the cic object described in the tree             *)
-(* It uses the previous functions and the to_cic_term method defined  *)
-(* in cicParser3 (used for subtrees that encode cic terms)            *)
-let rec get_term n =
- let module D = Pxp_document in
- let module C = Cic in
-  let ntype = n # node_type in
-  match ntype with
-    D.T_element "Definition" ->
-      let id = string_of_attr (n # attribute "name")
-      and params =
-       option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
-      and (value, typ) = 
-       let sons = n#sub_nodes in
-        match sons with
-          [v ; t] when
-            v#node_type = D.T_element "body" &&
-            t#node_type = D.T_element "type" ->
-             let v' = get_content v
-             and t' = get_content t in
-              (v'#extension#to_cic_term, t'#extension#to_cic_term)
-        | _ -> raise (IllFormedXml 6)
-      and xid = string_of_attr (n#attribute "id") in
-       let res = C.ADefinition (xid, ref None, id, value, typ, params) in
-        register_id xid res ;
-        res
-  | D.T_element "Axiom" ->
-      let id = string_of_attr (n # attribute "name")
-      and params = uri_list_of_attr (n # attribute "params")
-      and typ = 
-       (get_content (get_content n))#extension#to_cic_term
-      and xid = string_of_attr (n#attribute "id") in
-       let res = C.AAxiom (xid, ref None, id, typ, params) in
-        register_id xid res ;
-        res
-  | D.T_element "CurrentProof" ->
-     let name = string_of_attr (n#attribute "name")
-     and xid = string_of_attr (n#attribute "id") in
-     let sons = n#sub_nodes in
-      let (conjs, value, typ) = get_conjs_value_type sons in
-       let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
-        register_id xid res ;
-        res
-  | D.T_element "InductiveDefinition" ->
-     let sons = n#sub_nodes
-     and xid = string_of_attr (n#attribute "id") in
-      let inductiveTypes = get_inductive_types sons
-      and params = uri_list_of_attr (n#attribute "params")
-      and nparams = int_of_attr (n#attribute "noParams") in
-       let res =
-        C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
-       in
-        register_id xid res ;
-        res
-  | D.T_element "Variable" ->
-     let name = string_of_attr (n#attribute "name")
-     and xid = string_of_attr (n#attribute "id")
-     and (body, typ) = 
-      let sons = n#sub_nodes in
-       match sons with
-          [b ; t] when
-            b#node_type = D.T_element "body" &&
-            t#node_type = D.T_element "type" ->
-             let b' = get_content b
-             and t' = get_content t in
-              (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
-        | [t] when t#node_type = D.T_element "type" ->
-             let t' = get_content t in
-              (None, t'#extension#to_cic_term)
-        | _ -> raise (IllFormedXml 6)
-     in
-      let res = C.AVariable (xid,ref None,name,body,typ) in
-       register_id xid res ;
-       res
-  | D.T_element _
-  | D.T_data
-  | _ ->
-     raise (IllFormedXml 7)
-;;
diff --git a/helm/metadata/create2/touch/cicParser2.mli b/helm/metadata/create2/touch/cicParser2.mli
deleted file mode 100644 (file)
index be0a000..0000000
+++ /dev/null
@@ -1,57 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module is the objects level of a parser for cic objects from xml      *)
-(* files to the internal representation. It uses the module cicParser3        *)
-(* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
-(* level).                                                                    *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception IllFormedXml of int
-exception NotImplemented
-
-(* This is the main function and also the only one used directly from *)
-(* cicParser. Given the root of the dom tree, it returns the internal *)
-(* representation of the cic object described in the tree             *)
-(* It uses the previous functions and the to_cic_term method defined  *)
-(* in cicParser3 (used for subtrees that encode cic terms)            *)
-val get_term :
- < attribute : string -> Pxp_types.att_value;
-   node_type : Pxp_document.node_type;
-   sub_nodes : < attribute : string -> Pxp_types.att_value;
-                 node_type : Pxp_document.node_type;
-                 sub_nodes : CicParser3.cic_term Pxp_document.node list;
-                 .. >
-               list;
-   .. > ->
- Cic.annobj
diff --git a/helm/metadata/create2/touch/cicParser3.ml b/helm/metadata/create2/touch/cicParser3.ml
deleted file mode 100644 (file)
index ff356b1..0000000
+++ /dev/null
@@ -1,565 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module is the terms level of a parser for cic objects from xml        *)
-(* files to the internal representation. It is used by the module cicParser2  *)
-(* (objects level). It defines an extension of the standard dom using the     *)
-(* object-oriented extension machinery of markup: an object with a method     *)
-(* to_cic_term that returns the internal representation of the subtree is     *)
-(* added to each node of the dom tree                                         *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception IllFormedXml of int;;
-
-(* The hashtable from the current identifiers to the object or the terms *)
-let ids_to_targets = ref None;;
-
-(* The list of tokens of the current section path. *)
-(* Used to resolve relative URIs                   *)
-let current_sp = ref [];;
-
-(* The uri of the object been parsed *)
-let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
-
-(* True if annotation really matter *)
-let process_annotations = ref false;;
-
-(* Utility functions to map a markup attribute to something useful *)
-
-let cic_attr_of_xml_attr =
- function
-    Pxp_types.Value s       -> Cic.Name s
-  | Pxp_types.Implied_value -> Cic.Anonimous
-  | _             -> raise (IllFormedXml 1)
-
-let cic_sort_of_xml_attr =
- function
-    Pxp_types.Value "Prop" -> Cic.Prop
-  | Pxp_types.Value "Set"  -> Cic.Set
-  | Pxp_types.Value "Type" -> Cic.Type
-  | _            -> raise (IllFormedXml 2)
-
-let int_of_xml_attr =
- function
-    Pxp_types.Value n -> int_of_string n
-  | _       -> raise (IllFormedXml 3)
-
-let uri_of_xml_attr =
- function
-    Pxp_types.Value s -> UriManager.uri_of_string s
-  | _       -> raise (IllFormedXml 4)
-
-let string_of_xml_attr =
- function
-    Pxp_types.Value s -> s
-  | _       -> raise (IllFormedXml 5)
-
-let binder_of_xml_attr =
- function
-    Pxp_types.Value s -> if !process_annotations then Some s else None
-  | _       -> raise (IllFormedXml 17)
-;;
-
-let register_id id node =
- if !process_annotations then
-  match !ids_to_targets with
-     None -> assert false
-   | Some ids_to_targets ->
-      Hashtbl.add ids_to_targets id (Cic.Term node)
-;;
-
-(* the "interface" of the class linked to each node of the dom tree *)
-
-class virtual cic_term =
-  object (self)
-
-    (* fields and methods ever required by markup *)
-    val mutable node = (None : cic_term Pxp_document.node option)
-
-    method clone = {< >} 
-    method node =
-      match node with
-          None ->
-            assert false
-        | Some n -> n
-    method set_node n =
-      node <- Some n
-
-    (* a method that returns the internal representation of the tree (term) *)
-    (* rooted in this node                                                  *)
-    method virtual to_cic_term : Cic.annterm
-  end
-;;
-
-(* the class of the objects linked to nodes that are not roots of cic terms *)
-class eltype_not_of_cic =
-  object (self)
-
-     inherit cic_term
-
-     method to_cic_term = raise (IllFormedXml 6)
-  end
-;;
-
-(* the class of the objects linked to nodes whose content is a cic term *)
-(* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
-class eltype_transparent =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      match n#sub_nodes with
-         [ t ]  -> t#extension#to_cic_term
-       | _  -> raise (IllFormedXml 7)
-  end
-;;
-
-(* A class for each cic node type *)
-
-class eltype_fix =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let nofun = int_of_xml_attr (n#attribute "noFun")
-      and id = string_of_xml_attr (n#attribute "id")
-      and functions =
-       let sons = n#sub_nodes in
-        List.map
-         (function
-             f when f#node_type = Pxp_document.T_element "FixFunction" ->
-              let name = string_of_xml_attr (f#attribute "name")
-              and recindex = int_of_xml_attr (f#attribute "recIndex")
-              and (ty, body) =
-               match f#sub_nodes with
-                  [t ; b] when
-                    t#node_type = Pxp_document.T_element "type" &&
-                    b#node_type = Pxp_document.T_element "body" ->
-                     (t#extension#to_cic_term, b#extension#to_cic_term)
-                | _ -> raise (IllFormedXml 14)
-              in
-               (name, recindex, ty, body)
-           | _ -> raise (IllFormedXml 13)
-         ) sons
-      in
-       let res = Cic.AFix (id, ref None, nofun, functions) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_cofix =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let nofun = int_of_xml_attr (n#attribute "noFun")
-      and id = string_of_xml_attr (n#attribute "id")
-      and functions =
-       let sons = n#sub_nodes in
-        List.map
-         (function
-             f when f#node_type = Pxp_document.T_element "CofixFunction" ->
-              let name = string_of_xml_attr (f#attribute "name")
-              and (ty, body) =
-               match f#sub_nodes with
-                  [t ; b] when
-                    t#node_type = Pxp_document.T_element "type" &&
-                    b#node_type = Pxp_document.T_element "body" ->
-                     (t#extension#to_cic_term, b#extension#to_cic_term)
-                | _ -> raise (IllFormedXml 16)
-              in
-               (name, ty, body)
-           | _ -> raise (IllFormedXml 15)
-         ) sons
-      in
-       let res = Cic.ACoFix (id, ref None, nofun, functions) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_implicit =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let id = string_of_xml_attr (n#attribute "id") in
-       let res = Cic.AImplicit (id, ref None) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_rel =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let value  = int_of_xml_attr (n#attribute "value")
-      and binder = binder_of_xml_attr (n#attribute "binder")
-      and id = string_of_xml_attr (n#attribute "id") in
-       let res = Cic.ARel (id,ref None,value,binder) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_meta =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let value = int_of_xml_attr (n#attribute "no")
-      and id = string_of_xml_attr (n#attribute "id") in
-       let res = Cic.AMeta (id,ref None,value) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_var =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let name = string_of_xml_attr (n#attribute "relUri")
-      and xid = string_of_xml_attr (n#attribute "id") in
-       match Str.split (Str.regexp ",") name with
-          [index; id] ->
-           let get_prefix n =
-            let rec aux =
-             function
-                (0,_) -> "/"
-              | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
-              | _ -> raise (IllFormedXml 19)
-            in   
-             aux (List.length !current_sp - n,!current_sp)
-           in
-            let res =
-             Cic.AVar
-              (xid,ref None, 
-               (UriManager.uri_of_string
-                ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
-              )
-            in
-             register_id id res ;
-             res
-        | _ -> raise (IllFormedXml 18)
-  end
-;;
-
-class eltype_apply =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let children = n#sub_nodes
-      and id = string_of_xml_attr (n#attribute "id") in
-       if List.length children < 2 then raise (IllFormedXml 8)
-       else
-        let res =
-         Cic.AAppl
-          (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
-        in
-         register_id id res ;
-         res
-  end
-;;
-
-class eltype_cast =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let sons = n#sub_nodes
-      and id = string_of_xml_attr (n#attribute "id") in
-       match sons with
-          [te ; ty] when
-            te#node_type = Pxp_document.T_element "term" &&
-            ty#node_type = Pxp_document.T_element "type" ->
-             let term = te#extension#to_cic_term
-             and typ  = ty#extension#to_cic_term in
-              let res = Cic.ACast (id,ref None,term,typ) in
-               register_id id res ;
-               res
-        | _  -> raise (IllFormedXml 9)
-  end
-;;
-
-class eltype_sort =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let sort = cic_sort_of_xml_attr (n#attribute "value")
-      and id = string_of_xml_attr (n#attribute "id") in
-       let res = Cic.ASort (id,ref None,sort) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_abst =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let value = uri_of_xml_attr (n#attribute "uri")
-      and id = string_of_xml_attr (n#attribute "id") in
-       let res = Cic.AAbst (id,ref None,value) in
-        register_id id res ;
-        res
-  end
-;;
-
-class eltype_const =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let module U = UriManager in
-      let n = self#node in
-       let value = uri_of_xml_attr (n#attribute "uri")
-       and id = string_of_xml_attr (n#attribute "id") in
-        let res =
-         Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
-        in
-         register_id id res ;
-         res
-  end
-;;
-
-class eltype_mutind =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let module U = UriManager in
-      let n = self#node in
-       let name = uri_of_xml_attr (n#attribute "uri")
-       and noType = int_of_xml_attr (n#attribute "noType")
-       and id = string_of_xml_attr (n#attribute "id") in
-        let res =
-         Cic.AMutInd
-          (id,ref None,name, U.relative_depth !current_uri name 0, noType)
-        in
-         register_id id res ;
-         res
-  end
-;;
-
-class eltype_mutconstruct =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let module U = UriManager in
-      let n = self#node in
-       let name = uri_of_xml_attr (n#attribute "uri")
-       and noType = int_of_xml_attr (n#attribute "noType")
-       and noConstr = int_of_xml_attr (n#attribute "noConstr")
-       and id = string_of_xml_attr (n#attribute "id") in
-        let res = 
-         Cic.AMutConstruct
-          (id, ref None, name, U.relative_depth !current_uri name 0,
-          noType, noConstr)
-        in
-         register_id id res ;
-         res
-  end
-;;
-
-class eltype_prod =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let sons = n#sub_nodes
-      and id = string_of_xml_attr (n#attribute "id") in
-       match sons with
-          [s ; t] when
-            s#node_type = Pxp_document.T_element "source" &&
-            t#node_type = Pxp_document.T_element "target" ->
-             let name = cic_attr_of_xml_attr (t#attribute "binder")
-             and source = s#extension#to_cic_term
-             and target = t#extension#to_cic_term in
-              let res = Cic.AProd (id,ref None,name,source,target) in
-               register_id id res ;
-               res
-        | _  -> raise (IllFormedXml 10)
-  end
-;;
-
-class eltype_mutcase =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let module U = UriManager in
-      let n = self#node in
-       let sons = n#sub_nodes
-       and id = string_of_xml_attr (n#attribute "id") in
-        match sons with
-           ty::te::patterns when
-             ty#node_type = Pxp_document.T_element "patternsType" &&
-             te#node_type = Pxp_document.T_element "inductiveTerm" ->
-              let ci = uri_of_xml_attr (n#attribute "uriType")
-              and typeno = int_of_xml_attr (n#attribute "noType")
-              and inductiveType = ty#extension#to_cic_term
-              and inductiveTerm = te#extension#to_cic_term
-              and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
-              in
-               let res =
-                Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
-                 typeno,inductiveType,inductiveTerm,lpattern)
-               in
-                register_id id res ;
-                res
-         | _  -> raise (IllFormedXml 11)
-  end
-;;
-
-class eltype_lambda =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let sons = n#sub_nodes
-      and id = string_of_xml_attr (n#attribute "id") in
-       match sons with
-          [s ; t] when
-            s#node_type = Pxp_document.T_element "source" &&
-            t#node_type = Pxp_document.T_element "target" ->
-             let name = cic_attr_of_xml_attr (t#attribute "binder")
-             and source = s#extension#to_cic_term
-             and target = t#extension#to_cic_term in
-              let res = Cic.ALambda (id,ref None,name,source,target) in
-               register_id id res ;
-               res
-        | _  -> raise (IllFormedXml 12)
-  end
-;;
-
-class eltype_letin =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let sons = n#sub_nodes
-      and id = string_of_xml_attr (n#attribute "id") in
-       match sons with
-          [s ; t] when
-            s#node_type = Pxp_document.T_element "term" &&
-            t#node_type = Pxp_document.T_element "letintarget" ->
-             let name = cic_attr_of_xml_attr (t#attribute "binder")
-             and source = s#extension#to_cic_term
-             and target = t#extension#to_cic_term in
-              let res = Cic.ALetIn (id,ref None,name,source,target) in
-               register_id id res ;
-               res
-        | _  -> raise (IllFormedXml 12)
-  end
-;;
-
-(* The definition of domspec, an hashtable that maps each node type to the *)
-(* object that must be linked to it. Used by markup.                       *)
-
-let domspec =
- let module D = Pxp_document in
-  D.make_spec_from_alist
-   ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
-   ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
-   ~element_alist:
-    [ "REL",           (new D.element_impl (new eltype_rel)) ;
-      "VAR",           (new D.element_impl (new eltype_var)) ;
-      "META",          (new D.element_impl (new eltype_meta)) ;
-      "SORT",          (new D.element_impl (new eltype_sort)) ;
-      "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
-      "CAST",          (new D.element_impl (new eltype_cast)) ;
-      "PROD",          (new D.element_impl (new eltype_prod)) ;
-      "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
-      "LETIN",         (new D.element_impl (new eltype_letin)) ;
-      "APPLY",         (new D.element_impl (new eltype_apply)) ;
-      "CONST",         (new D.element_impl (new eltype_const)) ;
-      "ABST",          (new D.element_impl (new eltype_abst)) ;
-      "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
-      "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
-      "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
-      "FIX",           (new D.element_impl (new eltype_fix)) ;
-      "COFIX",         (new D.element_impl (new eltype_cofix)) ;
-      "arity",         (new D.element_impl (new eltype_transparent)) ;
-      "term",          (new D.element_impl (new eltype_transparent)) ;
-      "type",          (new D.element_impl (new eltype_transparent)) ;
-      "body",          (new D.element_impl (new eltype_transparent)) ;
-      "source",        (new D.element_impl (new eltype_transparent)) ;
-      "target",        (new D.element_impl (new eltype_transparent)) ;
-      "letintarget",   (new D.element_impl (new eltype_transparent)) ;
-      "patternsType",  (new D.element_impl (new eltype_transparent)) ;
-      "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
-      "pattern",       (new D.element_impl (new eltype_transparent))
-    ]
-   ()
-;;
diff --git a/helm/metadata/create2/touch/cicParser3.mli b/helm/metadata/create2/touch/cicParser3.mli
deleted file mode 100644 (file)
index ada1b2e..0000000
+++ /dev/null
@@ -1,67 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module is the terms level of a parser for cic objects from xml        *)
-(* files to the internal representation. It is used by the module cicParser2  *)
-(* (objects level). It defines an extension of the standard dom using the     *)
-(* object-oriented extension machinery of markup: an object with a method     *)
-(* to_cic_term that returns the internal representation of the subtree is     *)
-(* added to each node of the dom tree                                         *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception IllFormedXml of int
-
-val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref
-val current_sp : string list ref
-val current_uri : UriManager.uri ref
-val process_annotations : bool ref
-
-(* the "interface" of the class linked to each node of the dom tree *)
-class virtual cic_term :
-  object ('a)
-
-    (* fields and methods ever required by markup *)
-    val mutable node : cic_term Pxp_document.node option
-    method clone : 'a
-    method node : cic_term Pxp_document.node
-    method set_node : cic_term Pxp_document.node -> unit
-
-    (* a method that returns the internal representation of the tree (term) *)
-    (* rooted in this node                                                  *)
-    method virtual to_cic_term : Cic.annterm
-
-  end
-
-(* The definition of domspec, an hashtable that maps each node type to the *)
-(* object that must be linked to it. Used by markup.                       *)
-val domspec : cic_term Pxp_document.spec
diff --git a/helm/metadata/create2/touch/clientHTTP.ml b/helm/metadata/create2/touch/clientHTTP.ml
deleted file mode 100644 (file)
index 4d5488c..0000000
+++ /dev/null
@@ -1,60 +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://cs.unibo.it/helm/.
- *)
-
-exception HttpClientError of exn * string;;
-
-let send cmd =
- try
-  ignore (Http_client.Convenience.http_get cmd)
- with
-  e -> raise (HttpClientError (e,cmd))
-;;
-
-let get uri =
- try
-  Http_client.Convenience.http_get uri
- with
-  e -> raise (HttpClientError (e,uri))
-;;
-
-let get_and_save uri dest_filename =
- let reply = get uri
- and out_channel = open_out dest_filename in
-  output_string out_channel reply ;
-  close_out out_channel
-;;
-
-let get_and_save_to_tmp uri =
- let flat_string s s' c =
-  let cs = String.copy s in
-   for i = 0 to (String.length s) - 1 do
-    if String.contains s' s.[i] then cs.[i] <- c
-   done ;
-   cs
- in
-  let tmp_file = Configuration.tmp_dir ^ "/" ^ (flat_string uri ".-=:;!?/&" '_') in
-  get_and_save uri tmp_file ;
-  tmp_file
-;;
diff --git a/helm/metadata/create2/touch/clientHTTP.mli b/helm/metadata/create2/touch/clientHTTP.mli
deleted file mode 100644 (file)
index 59587ed..0000000
+++ /dev/null
@@ -1,30 +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://cs.unibo.it/helm/.
- *)
-
-exception HttpClientError of exn * string;;
-val send : string -> unit
-val get : string -> string
-val get_and_save : string -> string -> unit
-val get_and_save_to_tmp : string -> string
diff --git a/helm/metadata/create2/touch/configuration.ml.in b/helm/metadata/create2/touch/configuration.ml.in
deleted file mode 100644 (file)
index c743be1..0000000
+++ /dev/null
@@ -1,119 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 28/12/2000                                 *)
-(*                                                                            *)
-(* This is the parser that reads the configuration file of helm               *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception MalformedDir of string
-
-(* this should be the only hard coded constant *)
-let filename =
- let prefix =
-  try
-   Sys.getenv "HELM_CONFIGURATION_DIR"
-  with
-   Not_found -> "@HELM_CONFIGURATION_DIR@"
- in
-  if prefix.[(String.length prefix) - 1] = '/' then
-   raise (MalformedDir prefix) ;
-  prefix ^ "/configuration.xml";;
-
-exception Warnings;;
-
-class warner =
-  object 
-    method warn w =
-      print_endline ("WARNING: " ^ w) ;
-      (raise Warnings : unit)
-  end
-;;
-
-let xml_document () =
- let module Y = Pxp_yacc in
-  try 
-   let config = {Y.default_config with Y.warner = new warner} in
-    Y.parse_document_entity config (Y.from_file filename) Y.default_spec
-  with
-   e ->
-     print_endline (Pxp_types.string_of_exn e) ;
-     raise e
-;;
-
-exception Impossible;;
-
-let vars = Hashtbl.create 14;;
-
-(* resolve <value-of> tags and returns the string values of the variable tags *)
-let rec resolve =
- let module D = Pxp_document in
-  function
-     [] -> ""
-   | he::tl when he#node_type = D.T_element "value-of" ->
-      (match he#attribute "var" with
-          Pxp_types.Value var -> Hashtbl.find vars var
-        | _ -> raise Impossible
-      ) ^ resolve tl
-   | he::tl when he#node_type = D.T_data ->
-      he#data ^ resolve tl
-   | _ -> raise Impossible
-;;
-
-(* we trust the xml file to be valid because of the validating xml parser *)
-let _ =
- List.iter
-  (function
-      n ->
-       match n#node_type with
-          Pxp_document.T_element var ->
-           Hashtbl.add vars var (resolve (n#sub_nodes))
-        | _ -> raise Impossible
-  )
-  ((xml_document ())#root#sub_nodes)
-;;
-
-(* try to read a configuration variable, given its name into the
- * configuration.xml file and its name into the shell environment.
- * The shell variable, if present, has precedence over configuration.xml
- *)
-let read_configuration_var_env xml_name env_name =
- try
-  try
-   Sys.getenv env_name
-  with
-   Not_found -> Hashtbl.find vars xml_name
- with
-  Not_found ->
-   Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ;
-   flush stdout ;
-   raise Not_found
-
-let read_configuration_var xml_name =
- try
-  Hashtbl.find vars xml_name
- with
-  Not_found ->
-   Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ;
-   flush stdout ;
-   raise Not_found
-
-let helm_dir      = read_configuration_var     "helm_dir";;
-let dtd_dir       = read_configuration_var     "dtd_dir";;
-let style_dir     = read_configuration_var_env "style_dir" "HELM_STYLE_DIR";;
-let servers_file  = read_configuration_var     "servers_file";;
-let uris_dbm      = read_configuration_var     "uris_dbm";;
-let dest          = read_configuration_var     "dest";;
-let indexname     = read_configuration_var     "indexname";;
-let tmp_dir       = read_configuration_var     "tmp_dir"
-let helm_dir      = read_configuration_var     "helm_dir";;
-let getter_url    = read_configuration_var_env "getter_url" "HELM_GETTER_URL";;
-let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";;
-let annotations_dir = read_configuration_var_env "annotations_dir" "HELM_ANNOTATIONS_DIR"
-let annotations_url = read_configuration_var_env "annotations_url" "HELM_ANNOTATIONS_URL"
-
-let _ = Hashtbl.clear vars;;
-
diff --git a/helm/metadata/create2/touch/csc_pxp_reader.ml b/helm/metadata/create2/touch/csc_pxp_reader.ml
deleted file mode 100644 (file)
index 587c60c..0000000
+++ /dev/null
@@ -1,1008 +0,0 @@
-(* $Id$
- * ----------------------------------------------------------------------
- * PXP: The polymorphic XML parser for Objective Caml.
- * Copyright by Gerd Stolpmann. See LICENSE for details.
- *)
-
-open Pxp_types;;
-exception Not_competent;;
-exception Not_resolvable of exn;;
-
-class type resolver =
-  object
-    method init_rep_encoding : rep_encoding -> unit
-    method init_warner : collect_warnings -> unit
-    method rep_encoding : rep_encoding
-    method open_in : ext_id -> Lexing.lexbuf
-    method close_in : unit
-    method close_all : unit
-    method change_encoding : string -> unit
-    method clone : resolver
-  end
-;;
-
-
-class virtual resolve_general
- =
-  object (self)
-    val mutable internal_encoding = `Enc_utf8
-
-    val mutable encoding = `Enc_utf8
-    val mutable encoding_requested = false
-
-    val mutable warner = new drop_warnings
-
-    val mutable enc_initialized = false
-    val mutable wrn_initialized = false
-
-    val mutable clones = []
-
-    method init_rep_encoding e =
-      internal_encoding <- e;
-      enc_initialized <- true;
-
-    method init_warner w =
-      warner <- w;
-      wrn_initialized <- true;
-
-    method rep_encoding = (internal_encoding :> rep_encoding)
-
-(*
-    method clone =
-      ( {< encoding = `Enc_utf8;
-          encoding_requested = false;
-       >}
-       : # resolver :> resolver )
-*)
-
-    method private warn (k:int) =
-      (* Called if a character not representable has been found.
-       * k is the character code.
-       *)
-       if k < 0xd800 or (k >= 0xe000 & k <= 0xfffd) or
-          (k >= 0x10000 & k <= 0x10ffff) then begin
-            warner # warn ("Code point cannot be represented: " ^ string_of_int k);
-          end
-       else
-         raise (WF_error("Code point " ^ string_of_int k ^
-                   " outside the accepted range of code points"))
-
-
-    method private autodetect s =
-      (* s must be at least 4 bytes long. The slot 'encoding' is
-       * set to:
-       * "UTF-16-BE": UTF-16/UCS-2 encoding big endian
-       * "UTF-16-LE": UTF-16/UCS-2 encoding little endian
-       * "UTF-8":     UTF-8 encoding
-       *)
-      if String.length s < 4 then
-       encoding <- `Enc_utf8
-      else if String.sub s 0 2 = "\254\255" then
-       encoding <- `Enc_utf16
-         (* Note: Netconversion.recode will detect the big endianess, too *)
-      else if String.sub s 0 2 = "\255\254" then
-       encoding <- `Enc_utf16
-         (* Note: Netconversion.recode will detect the little endianess, too *)
-      else
-       encoding <- `Enc_utf8
-
-
-    method private virtual next_string : string -> int -> int -> int
-    method private virtual init_in : ext_id -> unit
-    method virtual close_in : unit
-
-    method close_all =
-      List.iter (fun r -> r # close_in) clones
-
-    method open_in xid =
-      assert(enc_initialized && wrn_initialized);
-
-      encoding <- `Enc_utf8;
-      encoding_requested <- false;
-      self # init_in xid;         (* may raise Not_competent *)
-      (* init_in: may already set 'encoding' *)
-
-      let buffer_max = 512 in
-      let buffer = String.make buffer_max ' ' in
-      let buffer_len = ref 0 in
-      let buffer_end = ref false in
-      let fillup () =
-       if not !buffer_end & !buffer_len < buffer_max then begin
-         let l =
-           self # next_string buffer !buffer_len (buffer_max - !buffer_len) in
-         if l = 0 then
-           buffer_end := true
-         else begin
-           buffer_len := !buffer_len + l
-         end
-       end
-      in
-      let consume n =
-       let l = !buffer_len - n in
-       String.blit buffer n buffer 0 l;
-       buffer_len := l
-      in
-
-      fillup();
-      if not encoding_requested then self # autodetect buffer;
-
-      Lexing.from_function
-       (fun s n ->
-          (* TODO: if encoding = internal_encoding, it is possible to
-           * avoid copying buffer to s because s can be directly used
-           * as buffer.
-           *)
-
-          fillup();
-          if !buffer_len = 0 then
-            0
-          else begin
-            let m_in  = !buffer_len in
-            let m_max = if encoding_requested then n else 1 in
-            let n_in, n_out, encoding' =
-              if encoding = (internal_encoding : rep_encoding :> encoding) &&
-                 encoding_requested
-              then begin
-                (* Special case encoding = internal_encoding *)
-                String.blit buffer 0 s 0 m_in;
-                m_in, m_in, encoding
-              end
-              else
-                Netconversion.recode
-                  ~in_enc:encoding
-                  ~in_buf:buffer
-                  ~in_pos:0
-                  ~in_len:m_in
-                  ~out_enc:(internal_encoding : rep_encoding :> encoding)
-                  ~out_buf:s
-                  ~out_pos:0
-                  ~out_len:n
-                  ~max_chars:m_max
-                  ~subst:(fun k -> self # warn k; "")
-            in
-            if n_in = 0 then
-              (* An incomplete character at the end of the stream: *)
-              raise Netconversion.Malformed_code;
-              (* failwith "Badly encoded character"; *)
-            encoding <- encoding';
-            consume n_in;
-            assert(n_out <> 0);
-            n_out
-          end)
-
-    method change_encoding enc =
-      if not encoding_requested then begin
-       if enc <> "" then begin
-         match Netconversion.encoding_of_string enc with
-             `Enc_utf16 ->
-               (match encoding with
-                    (`Enc_utf16_le | `Enc_utf16_be) -> ()
-                  | `Enc_utf16 -> assert false
-                  | _ ->
-                      raise(WF_error "Encoding of data stream and encoding declaration mismatch")
-               )
-           | e ->
-               encoding <- e
-       end;
-       (* else: the autodetected encoding counts *)
-       encoding_requested <- true;
-      end;
-  end
-;;
-
-
-class resolve_read_any_channel ?(close=close_in) ~channel_of_id () =
-  object (self)
-    inherit resolve_general as super
-
-    val f_open = channel_of_id
-    val mutable current_channel = None
-    val close = close
-
-    method private init_in (id:ext_id) =
-      if current_channel <> None then
-       failwith "Pxp_reader.resolve_read_any_channel # init_in";
-      let ch, enc_opt = f_open id in       (* may raise Not_competent *)
-      begin match enc_opt with
-         None     -> ()
-       | Some enc -> encoding <- enc; encoding_requested <- true
-      end;
-      current_channel <- Some ch;
-
-    method private next_string s ofs len =
-      match current_channel with
-         None -> failwith "Pxp_reader.resolve_read_any_channel # next_string"
-       | Some ch ->
-           input ch s ofs len
-
-    method close_in =
-      match current_channel with
-         None -> ()
-       | Some ch ->
-           close ch;
-           current_channel <- None
-
-    method clone =
-      let c = new resolve_read_any_channel
-               ?close:(Some close) f_open () in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      (c :> resolver)
-
-  end
-;;
-
-
-class resolve_read_this_channel1 is_stale ?id ?fixenc ?close ch =
-
-  let getchannel = ref (fun xid -> assert false) in
-
-  object (self)
-    inherit resolve_read_any_channel
-              ?close
-             (fun xid -> !getchannel xid)
-             ()
-             as super
-
-    val mutable is_stale = is_stale
-      (* The channel can only be read once. To avoid that the channel
-       * is opened several times, the flag 'is_stale' is set after the
-       * first time.
-       *)
-
-    val fixid = id
-    val fixenc = fixenc
-    val fixch = ch
-
-    initializer
-      getchannel := self # getchannel
-
-    method private getchannel xid =
-      begin match fixid with
-         None -> ()
-       | Some bound_xid ->
-           if xid <> bound_xid then raise Not_competent
-      end;
-      ch, fixenc
-
-    method private init_in (id:ext_id) =
-      if is_stale then
-       raise Not_competent
-      else begin
-       super # init_in id;
-       is_stale <- true
-      end
-
-    method close_in =
-      current_channel <- None
-
-    method clone =
-      let c = new resolve_read_this_channel1
-               is_stale
-               ?id:fixid ?fixenc:fixenc ?close:(Some close) fixch
-      in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      (c :> resolver)
-
-  end
-;;
-
-
-class resolve_read_this_channel =
-  resolve_read_this_channel1 false
-;;
-
-
-class resolve_read_any_string ~string_of_id () =
-  object (self)
-    inherit resolve_general as super
-
-    val f_open = string_of_id
-    val mutable current_string = None
-    val mutable current_pos    = 0
-
-    method private init_in (id:ext_id) =
-      if current_string <> None then
-       failwith "Pxp_reader.resolve_read_any_string # init_in";
-      let s, enc_opt = f_open id in       (* may raise Not_competent *)
-      begin match enc_opt with
-         None     -> ()
-       | Some enc -> encoding <- enc; encoding_requested <- true
-      end;
-      current_string <- Some s;
-      current_pos    <- 0;
-
-    method private next_string s ofs len =
-      match current_string with
-         None -> failwith "Pxp_reader.resolve_read_any_string # next_string"
-       | Some str ->
-           let l = min len (String.length str - current_pos) in
-           String.blit str current_pos s ofs l;
-           current_pos <- current_pos + l;
-           l
-
-    method close_in =
-      match current_string with
-         None -> ()
-       | Some _ ->
-           current_string <- None
-
-    method clone =
-      let c = new resolve_read_any_string f_open () in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      (c :> resolver)
-  end
-;;
-
-
-class resolve_read_this_string1 is_stale ?id ?fixenc str =
-
-  let getstring = ref (fun xid -> assert false) in
-
-  object (self)
-    inherit resolve_read_any_string (fun xid -> !getstring xid) () as super
-
-    val is_stale = is_stale
-      (* For some reasons, it is not allowed to open a clone of the resolver
-       * a second time when the original resolver is already open.
-       *)
-
-    val fixid = id
-    val fixenc = fixenc
-    val fixstr = str
-
-    initializer
-      getstring := self # getstring
-
-    method private getstring xid =
-      begin match fixid with
-         None -> ()
-       | Some bound_xid ->
-           if xid <> bound_xid then raise Not_competent
-      end;
-      fixstr, fixenc
-
-
-    method private init_in (id:ext_id) =
-      if is_stale then
-       raise Not_competent
-      else
-       super # init_in id
-
-    method clone =
-      let c = new resolve_read_this_string1
-               (is_stale or current_string <> None)
-               ?id:fixid ?fixenc:fixenc fixstr
-      in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      (c :> resolver)
-  end
-;;
-
-
-class resolve_read_this_string =
-  resolve_read_this_string1 false
-;;
-
-
-class resolve_read_url_channel
-  ?(base_url = Neturl.null_url)
-  ?close
-  ~url_of_id
-  ~channel_of_url
-  ()
-
-  : resolver
-  =
-
-  let getchannel = ref (fun xid -> assert false) in
-
-  object (self)
-    inherit resolve_read_any_channel
-              ?close
-             (fun xid -> !getchannel xid)
-             ()
-             as super
-
-    val base_url = base_url
-    val mutable own_url = Neturl.null_url
-
-    val url_of_id = url_of_id
-    val channel_of_url = channel_of_url
-
-
-    initializer
-      getchannel := self # getchannel
-
-    method private getchannel xid =
-      let rel_url = url_of_id xid in    (* may raise Not_competent *)
-
-      try
-       (* Now compute the absolute URL: *)
-       let abs_url = 
-         if Neturl.url_provides ~scheme:true rel_url then
-           rel_url
-         else
-           Neturl.apply_relative_url base_url rel_url in
-            (* may raise Malformed_URL *)
-
-       (* Simple check whether 'abs_url' is really absolute: *)
-       if not(Neturl.url_provides ~scheme:true abs_url)
-       then raise Not_competent;
-
-       own_url <- abs_url;
-        (* FIXME: Copy 'abs_url' ? *)
-
-       (* Get and return the channel: *)
-       channel_of_url xid abs_url            (* may raise Not_competent *)
-      with
-         Neturl.Malformed_URL -> raise (Not_resolvable Neturl.Malformed_URL)
-       | Not_competent        -> raise (Not_resolvable Not_found)
-
-    method clone =
-      let c =
-       new resolve_read_url_channel
-         ?base_url:(Some own_url)
-         ?close:(Some close)
-         ~url_of_id:url_of_id
-         ~channel_of_url:channel_of_url
-         ()
-      in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      (c :> resolve_read_url_channel)
-  end
-;;
-
-
-type spec = [ `Not_recognized | `Allowed | `Required ]
-
-class resolve_as_file
-  ?(file_prefix = (`Allowed :> spec))
-  ?(host_prefix = (`Allowed :> spec))
-  ?(system_encoding = `Enc_utf8)
-  ?(map_private_id = (fun _ -> raise Not_competent))
-  ?(open_private_id = (fun _ -> raise Not_competent))
-  ()
-  =
-
-  let url_syntax =
-    let enable_if =
-      function
-         `Not_recognized  -> Neturl.Url_part_not_recognized
-       | `Allowed         -> Neturl.Url_part_allowed
-       | `Required        -> Neturl.Url_part_required
-    in
-    { Neturl.null_url_syntax with
-       Neturl.url_enable_scheme = enable_if file_prefix;
-       Neturl.url_enable_host   = enable_if host_prefix;
-       Neturl.url_enable_path   = Neturl.Url_part_required;
-       Neturl.url_accepts_8bits = true;
-    }
-  in
-
-  let base_url_syntax =
-    { Neturl.null_url_syntax with
-       Neturl.url_enable_scheme = Neturl.Url_part_required;
-       Neturl.url_enable_host   = Neturl.Url_part_allowed;
-       Neturl.url_enable_path   = Neturl.Url_part_required;
-       Neturl.url_accepts_8bits = true;
-    }
-  in
-
-  let default_base_url =
-    Neturl.make_url
-      ~scheme: "file"
-      ~host:   ""
-      ~path:   (Neturl.split_path (Sys.getcwd() ^ "/"))
-      base_url_syntax
-  in
-
-  let file_url_of_id xid =
-    let file_url_of_sysname sysname =
-      (* By convention, we can assume that sysname is a URL conforming
-       * to RFC 1738 with the exception that it may contain non-ASCII
-       * UTF-8 characters.
-       *)
-      try
-       Neturl.url_of_string url_syntax sysname
-          (* may raise Malformed_URL *)
-      with
-         Neturl.Malformed_URL -> raise Not_competent
-    in
-    let url =
-      match xid with
-         Anonymous          -> raise Not_competent
-       | Public (_,sysname) -> if sysname <> "" then file_url_of_sysname sysname
-                                                 else raise Not_competent
-       | System sysname     -> file_url_of_sysname sysname
-       | Private pid        -> map_private_id pid
-    in
-    let scheme =
-      try Neturl.url_scheme url with Not_found -> "file" in
-    let host =
-      try Neturl.url_host url with Not_found -> "" in
-
-    if scheme <> "file" then raise Not_competent;
-    if host <> "" && host <> "localhost" then raise Not_competent;
-
-    url
-  in
-
-  let channel_of_file_url xid url =
-    match xid with
-       Private pid -> open_private_id pid
-      | _ ->
-         ( try
-             let path_utf8 =
-               try Neturl.join_path (Neturl.url_path ~encoded:false url)
-               with Not_found -> raise Not_competent
-             in
-             
-             let path =
-               Netconversion.recode_string
-                 ~in_enc:  `Enc_utf8
-                 ~out_enc: system_encoding
-                 path_utf8 in
-              (* May raise Malformed_code *)
-             
-             open_in_bin path, None
-               (* May raise Sys_error *)
-               
-           with
-             | Netconversion.Malformed_code -> assert false
-               (* should not happen *)
-             | Sys_error _ as e ->
-                 raise (Not_resolvable e)
-         )
-  in
-
-  resolve_read_url_channel
-    ~base_url:       default_base_url
-    ~url_of_id:      file_url_of_id
-    ~channel_of_url: channel_of_file_url
-    ()
-;;
-
-
-let make_file_url ?(system_encoding = `Enc_utf8) ?(enc = `Enc_utf8) filename =
-  let utf8_filename =
-    Netconversion.recode_string
-    ~in_enc: enc
-    ~out_enc: `Enc_utf8 
-      filename
-  in
-
-  let utf8_abs_filename =
-    if utf8_filename <> "" && utf8_filename.[0] = '/' then
-      utf8_filename
-    else
-      let cwd = Sys.getcwd() in
-      let cwd_utf8 =
-       Netconversion.recode_string
-       ~in_enc: system_encoding
-       ~out_enc: `Enc_utf8 in
-      cwd ^ "/" ^ utf8_filename
-  in
-  
-  let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in
-  let url = Neturl.make_url
-           ~scheme:"file"
-           ~host:"localhost"
-           ~path:(Neturl.split_path utf8_abs_filename)
-             syntax
-  in
-  url
-;;
-
-
-class lookup_public_id (catalog : (string * resolver) list) =
-  let norm_catalog =
-    List.map (fun (id,s) -> Pxp_aux.normalize_public_id id, s) catalog in
-( object (self)
-    val cat = norm_catalog
-    val mutable internal_encoding = `Enc_utf8
-    val mutable warner = new drop_warnings
-    val mutable active_resolver = None
-
-    method init_rep_encoding enc =
-      internal_encoding <- enc
-
-    method init_warner w =
-      warner <- w;
-
-    method rep_encoding = internal_encoding
-      (* CAUTION: This may not be the truth! *)
-
-    method open_in xid =
-
-      if active_resolver <> None then failwith "Pxp_reader.lookup_* # open_in";
-
-      let r =
-       match xid with
-           Public(pubid,_) ->
-             begin
-               (* Search pubid in catalog: *)
-               try
-                 let norm_pubid = Pxp_aux.normalize_public_id pubid in
-                 List.assoc norm_pubid cat
-               with
-                   Not_found ->
-                     raise Not_competent
-             end
-         | _ ->
-             raise Not_competent
-      in
-
-      let r' = r # clone in
-      r' # init_rep_encoding internal_encoding;
-      r' # init_warner warner;
-      let lb = r' # open_in xid in   (* may raise Not_competent *)
-      active_resolver <- Some r';
-      lb
-
-    method close_in =
-      match active_resolver with
-         None   -> ()
-       | Some r -> r # close_in;
-                   active_resolver <- None
-
-    method close_all =
-      self # close_in
-
-    method change_encoding (enc:string) =
-      match active_resolver with
-         None   -> failwith "Pxp_reader.lookup_* # change_encoding"
-       | Some r -> r # change_encoding enc
-
-    method clone =
-      let c = new lookup_public_id cat in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      c
-  end : resolver )
-;;
-
-
-let lookup_public_id_as_file ?(fixenc:encoding option) catalog =
-  let ch_of_id filename id =
-    let ch = open_in_bin filename in  (* may raise Sys_error *)
-    ch, fixenc
-  in
-  let catalog' =
-    List.map
-      (fun (id,s) ->
-        (id, new resolve_read_any_channel (ch_of_id s) ())
-      )
-      catalog
-  in
-  new lookup_public_id catalog'
-;;
-
-
-let lookup_public_id_as_string ?(fixenc:encoding option) catalog =
-   let catalog' =
-    List.map
-      (fun (id,s) ->
-        (id, new resolve_read_any_string (fun _ -> s, fixenc) ())
-      )
-      catalog
-  in
-  new lookup_public_id catalog'
-;;
-   
-
-class lookup_system_id (catalog : (string * resolver) list) =
-( object (self)
-    val cat = catalog
-    val mutable internal_encoding = `Enc_utf8
-    val mutable warner = new drop_warnings
-    val mutable active_resolver = None
-
-    method init_rep_encoding enc =
-      internal_encoding <- enc
-
-    method init_warner w =
-      warner <- w;
-
-    method rep_encoding = internal_encoding
-      (* CAUTION: This may not be the truth! *)
-
-
-    method open_in xid =
-
-      if active_resolver <> None then failwith "Pxp_reader.lookup_system_id # open_in";
-
-      let lookup sysid =
-       try
-         List.assoc sysid cat
-       with
-           Not_found ->
-             raise Not_competent
-      in
-
-      let r =
-       match xid with
-           System sysid    -> lookup sysid
-         | Public(_,sysid) -> lookup sysid
-         | _               -> raise Not_competent
-      in
-
-      let r' = r # clone in
-      r' # init_rep_encoding internal_encoding;
-      r' # init_warner warner;
-      let lb = r' # open_in xid in   (* may raise Not_competent *)
-      active_resolver <- Some r';
-      lb
-
-
-    method close_in =
-      match active_resolver with
-         None   -> ()
-       | Some r -> r # close_in;
-                   active_resolver <- None
-
-    method close_all =
-      self # close_in
-
-    method change_encoding (enc:string) =
-      match active_resolver with
-         None   -> failwith "Pxp_reader.lookup_system # change_encoding"
-       | Some r -> r # change_encoding enc
-
-    method clone =
-      let c = new lookup_system_id cat in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      c
-  end : resolver)
-;;
-
-
-let lookup_system_id_as_file ?(fixenc:encoding option) catalog =
-  let ch_of_id filename id =
-    let ch = open_in_bin filename in  (* may raise Sys_error *)
-    ch, fixenc
-  in
-  let catalog' =
-    List.map
-      (fun (id,s) ->
-        (id, new resolve_read_any_channel (ch_of_id s) ())
-      )
-      catalog
-  in
-  new lookup_system_id catalog'
-;;
-
-
-let lookup_system_id_as_string ?(fixenc:encoding option) catalog =
-   let catalog' =
-    List.map
-      (fun (id,s) ->
-        (id, new resolve_read_any_string (fun _ -> s, fixenc) ())
-      )
-      catalog
-  in
-  new lookup_system_id catalog'
-;;
-   
-
-type combination_mode =
-    Public_before_system
-  | System_before_public
-;;
-
-
-class combine ?prefer ?(mode = Public_before_system) rl =
-  object (self)
-    val prefered_resolver = prefer
-    val mode = mode
-    val resolvers = (rl : resolver list)
-    val mutable internal_encoding = `Enc_utf8
-    val mutable warner = new drop_warnings
-    val mutable active_resolver = None
-    val mutable clones = []
-
-    method init_rep_encoding enc =
-      List.iter
-       (fun r -> r # init_rep_encoding enc)
-       rl;
-      internal_encoding <- enc
-
-    method init_warner w =
-      List.iter
-       (fun r -> r # init_warner w)
-       rl;
-      warner <- w;
-
-    method rep_encoding = internal_encoding
-      (* CAUTION: This may not be the truth! *)
-
-    method open_in xid =
-      let rec find_competent_resolver_for xid' rl =
-       match rl with
-           r :: rl' ->
-             begin try
-               r, (r # open_in xid')
-             with
-                 Not_competent -> find_competent_resolver_for xid' rl'
-             end;
-         | [] ->
-             raise Not_competent
-      in
-
-      let find_competent_resolver rl =
-       match xid with
-           Public(pubid,sysid) ->
-             ( match mode with
-                   Public_before_system ->
-                     ( try
-                         find_competent_resolver_for(Public(pubid,"")) rl
-                       with
-                           Not_competent ->
-                             find_competent_resolver_for(System sysid) rl
-                     )
-                 | System_before_public ->
-                     ( try
-                         find_competent_resolver_for(System sysid) rl
-                       with
-                           Not_competent ->
-                             find_competent_resolver_for(Public(pubid,"")) rl
-                     )
-             )
-         | other ->
-             find_competent_resolver_for other rl
-      in
-
-      if active_resolver <> None then failwith "Pxp_reader.combine # open_in";
-      let r, lb =
-       match prefered_resolver with
-           None ->   find_competent_resolver resolvers
-         | Some r -> find_competent_resolver (r :: resolvers)
-      in
-      active_resolver <- Some r;
-      lb
-
-    method close_in =
-      match active_resolver with
-         None   -> ()
-       | Some r -> r # close_in;
-                   active_resolver <- None
-
-    method close_all =
-      List.iter (fun r -> r # close_in) clones
-
-    method change_encoding (enc:string) =
-      match active_resolver with
-         None   -> failwith "Pxp_reader.combine # change_encoding"
-       | Some r -> r # change_encoding enc
-
-    method clone =
-      let c =
-       match active_resolver with
-           None   ->
-             new combine ?prefer:None ?mode:(Some mode) 
-                          (List.map (fun q -> q # clone) resolvers)
-         | Some r ->
-             let r' = r # clone in
-             new combine
-               ?prefer:(Some r')
-               ?mode:(Some mode)
-               (List.map
-                  (fun q -> if q == r then r' else q # clone)
-                  resolvers)
-      in
-      c # init_rep_encoding internal_encoding;
-      c # init_warner warner;
-      clones <- c :: clones;
-      c
-  end
-
-
-
-(* ======================================================================
- * History:
- *
- * $Log$
- * Revision 1.1  2001/10/24 15:33:16  sacerdot
- * New procedure to create metadata committed and old procedure removed.
- * The new procedure is based on ocaml code and builds metadata for both
- * forward and backward pointers. The old one was based on a stylesheet.
- *
- * Revision 1.16  2001/07/01 09:46:40  gerd
- *     Fix: resolve_read_url_channel does not use the base_url if
- * the current URL is already absolute
- *
- * Revision 1.15  2001/07/01 08:35:23  gerd
- *     Instead of the ~auto_close argument, there is now a
- * ~close argument for several functions/classes. This allows some
- * additional action when the resolver is closed.
- *
- * Revision 1.14  2001/06/14 23:28:02  gerd
- *     Fix: class combine works now with private IDs.
- *
- * Revision 1.13  2001/04/22 14:16:48  gerd
- *     resolve_as_file: you can map private IDs to arbitrary channels.
- *     resolve_read_url_channel: changed type of the channel_of_url
- * argument (ext_id is also passed)
- *     More examples and documentation.
- *
- * Revision 1.12  2001/04/21 17:40:48  gerd
- *     Bugfix in 'combine'
- *
- * Revision 1.11  2001/04/03 20:22:44  gerd
- *     New resolvers for catalogs of PUBLIC and SYSTEM IDs.
- *     Improved "combine": PUBLIC and SYSTEM IDs are handled
- * separately.
- *     Rewritten from_file: Is now a simple application of the
- * Pxp_reader classes and functions. (The same has still to be done
- * for from_channel!)
- *
- * Revision 1.10  2001/02/01 20:38:49  gerd
- *     New support for PUBLIC identifiers.
- *
- * Revision 1.9  2000/08/14 22:24:55  gerd
- *     Moved the module Pxp_encoding to the netstring package under
- * the new name Netconversion.
- *
- * Revision 1.8  2000/07/16 18:31:09  gerd
- *     The exception Illegal_character has been dropped.
- *
- * Revision 1.7  2000/07/09 15:32:01  gerd
- *     Fix in resolve_this_channel, resolve_this_string
- *
- * Revision 1.6  2000/07/09 01:05:33  gerd
- *     New methode 'close_all' that closes the clones, too.
- *
- * Revision 1.5  2000/07/08 16:24:56  gerd
- *     Introduced the exception 'Not_resolvable' to indicate that
- * 'combine' should not try the next resolver of the list.
- *
- * Revision 1.4  2000/07/06 23:04:46  gerd
- *     Quick fix for 'combine': The active resolver is "prefered",
- * but the other resolvers are also used.
- *
- * Revision 1.3  2000/07/06 21:43:45  gerd
- *     Fix: Public(_,name) is now treated as System(name) if
- * name is non-empty.
- *
- * Revision 1.2  2000/07/04 22:13:30  gerd
- *     Implemented the new API rev. 1.2 of pxp_reader.mli.
- *
- * Revision 1.1  2000/05/29 23:48:38  gerd
- *     Changed module names:
- *             Markup_aux          into Pxp_aux
- *             Markup_codewriter   into Pxp_codewriter
- *             Markup_document     into Pxp_document
- *             Markup_dtd          into Pxp_dtd
- *             Markup_entity       into Pxp_entity
- *             Markup_lexer_types  into Pxp_lexer_types
- *             Markup_reader       into Pxp_reader
- *             Markup_types        into Pxp_types
- *             Markup_yacc         into Pxp_yacc
- * See directory "compatibility" for (almost) compatible wrappers emulating
- * Markup_document, Markup_dtd, Markup_reader, Markup_types, and Markup_yacc.
- *
- * ======================================================================
- * Old logs from markup_reader.ml:
- *
- * Revision 1.3  2000/05/29 21:14:57  gerd
- *     Changed the type 'encoding' into a polymorphic variant.
- *
- * Revision 1.2  2000/05/20 20:31:40  gerd
- *     Big change: Added support for various encodings of the
- * internal representation.
- *
- * Revision 1.1  2000/03/13 23:41:44  gerd
- *     Initial revision; this code was formerly part of Markup_entity.
- *
- *
- *)
diff --git a/helm/metadata/create2/touch/deannotate.ml b/helm/metadata/create2/touch/deannotate.ml
deleted file mode 100644 (file)
index 00d4854..0000000
+++ /dev/null
@@ -1,98 +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://cs.unibo.it/helm/.
- *)
-
-let expect_possible_parameters = ref false;;
-
-exception NotExpectingPossibleParameters;;
-
-let rec deannotate_term =
- let module C = Cic in
-  function
-     C.ARel (_,_,n,_) -> C.Rel n
-   | C.AVar (_,_,uri) -> C.Var uri
-   | C.AMeta (_,_,n) -> C.Meta n
-   | C.ASort (_,_,s) -> C.Sort s
-   | C.AImplicit _ -> C.Implicit
-   | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
-   | C.AProd (_,_,name,so,ta) ->
-      C.Prod (name, deannotate_term so, deannotate_term ta)
-   | C.ALambda (_,_,name,so,ta) ->
-      C.Lambda (name, deannotate_term so, deannotate_term ta)
-   | C.ALetIn (_,_,name,so,ta) ->
-      C.LetIn (name, deannotate_term so, deannotate_term ta)
-   | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l)
-   | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno)
-   | C.AAbst (_,_,uri) -> C.Abst uri
-   | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
-   | C.AMutConstruct (_,_,uri,cookingsno,i,j) ->
-      C.MutConstruct (uri,cookingsno,i,j)
-   | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) ->
-      C.MutCase (uri,cookingsno,i,deannotate_term outtype,
-       deannotate_term te, List.map deannotate_term pl)
-   | C.AFix (_,_,funno,ifl) ->
-      C.Fix (funno, List.map deannotate_inductiveFun ifl)
-   | C.ACoFix (_,_,funno,ifl) ->
-      C.CoFix (funno, List.map deannotate_coinductiveFun ifl)
-
-and deannotate_inductiveFun (name,index,ty,bo) =
- (name, index, deannotate_term ty, deannotate_term bo)
-
-and deannotate_coinductiveFun (name,ty,bo) =
- (name, deannotate_term ty, deannotate_term bo)
-;;
-
-let deannotate_inductiveType (name, isinductive, arity, cons) =
- (name, isinductive, deannotate_term arity,
-  List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons)
-;;
-
-let deannotate_obj =
- let module C = Cic in
-  function
-     C.ADefinition (_, _, id, bo, ty, params) ->
-      (match params with
-          C.Possible params ->
-           if !expect_possible_parameters then
-            C.Definition (id, deannotate_term bo, deannotate_term ty, params)
-           else
-            raise NotExpectingPossibleParameters
-        | C.Actual params ->
-           C.Definition (id, deannotate_term bo, deannotate_term ty, params)
-      )
-   | C.AAxiom (_, _, id, ty, params) ->
-      C.Axiom (id, deannotate_term ty, params)
-   | C.AVariable (_, _, name, bo, ty) ->
-      C.Variable (name,
-       (match bo with None -> None | Some bo -> Some (deannotate_term bo)),
-       deannotate_term ty)
-   | C.ACurrentProof (_, _, name, conjs, bo, ty) ->
-      C.CurrentProof (
-       name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
-       deannotate_term bo, deannotate_term ty
-      )
-   | C.AInductiveDefinition (_, _, tys, params, parno) ->
-      C.InductiveDefinition ( List.map deannotate_inductiveType tys,
-       params, parno)
-;;
diff --git a/helm/metadata/create2/touch/getter.ml b/helm/metadata/create2/touch/getter.ml
deleted file mode 100644 (file)
index 894bf3e..0000000
+++ /dev/null
@@ -1,63 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(******************************************************************************)
-
-let getter_url = ref Configuration.getter_url;;
-
-let update () =
- (* deliver update request to http_getter *)
- ClientHTTP.send (!getter_url ^ "update")
-;;
-
-type format =
-   Normal
- | GZipped
-;;
-
-let getxml ?(format=Normal) ?(patchdtd=true) uri =
- (* deliver getxml request to http_getter *)
- ClientHTTP.get_and_save_to_tmp
-  (!getter_url ^ "getxml" ^
-    "?uri=" ^ UriManager.string_of_uri uri ^
-    "&format=" ^ (match format with Normal -> "normal" | GZipped -> "gzipped") ^
-    "&patch_dtd=" ^ (match patchdtd with true -> "yes" | false -> "no")
-  )
-;;
-
-let register uri url =
- (* deliver register request to http_getter *)
- ClientHTTP.send
-  (!getter_url ^ "register" ^
-    "?uri=" ^ (UriManager.string_of_uri uri) ^
-    "&url=" ^ url)
-;;
diff --git a/helm/metadata/create2/touch/getter.mli b/helm/metadata/create2/touch/getter.mli
deleted file mode 100644 (file)
index 6b1d2ca..0000000
+++ /dev/null
@@ -1,53 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* THE URL OF THE HTTP GETTER *)
-val getter_url : string ref
-
-(* SIMPLE BINDINGS TO THE HTTP GETTER *)
-(* synchronize with the servers *)
-val update : unit -> unit
-
-type format =
-   Normal
- | GZipped
-;;
-
-(* get the xml file                              *)
-(* defaults: format = Normal and patchdtd = true *)
-val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string
-
-(* adds an (URI -> URL) entry in the map from URIs to URLs *)
-val register : UriManager.uri -> string -> unit
diff --git a/helm/metadata/create2/touch/pxpUriResolver.ml b/helm/metadata/create2/touch/pxpUriResolver.ml
deleted file mode 100644 (file)
index 1e2fec9..0000000
+++ /dev/null
@@ -1,266 +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://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 11/10/2000                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-let resolve s =
- let starts_with s s' =
-  if String.length s < String.length s' then
-   false
-  else
-   (String.sub s 0 (String.length s')) = s'
- in
-  if starts_with s "http:" then
-   ClientHTTP.get_and_save_to_tmp s
-  else
-   s
-;;
-
-(*PXP 1.0
-let url_syntax =
-    let enable_if =
-      function
-         `Not_recognized  -> Neturl.Url_part_not_recognized
-       | `Allowed         -> Neturl.Url_part_allowed
-       | `Required        -> Neturl.Url_part_required
-    in
-    { Neturl.null_url_syntax with
-       Neturl.url_enable_scheme = enable_if `Allowed;
-       Neturl.url_enable_host   = enable_if `Allowed;
-       Neturl.url_enable_path   = Neturl.Url_part_required;
-       Neturl.url_accepts_8bits = true;
-    } 
-;;
-
-exception Unexpected;; (* Added when porting the file to PXP 1.1 *)
-
-let file_url_of_id xid =
-  let file_url_of_sysname sysname =
-    (* By convention, we can assume that sysname is a URL conforming
-     * to RFC 1738 with the exception that it may contain non-ASCII
-     * UTF-8 characters. 
-     *)
-    try
-     Neturl.url_of_string url_syntax sysname 
-        (* may raise Malformed_URL *)
-    with
-     Neturl.Malformed_URL -> raise Pxp_reader.Not_competent
-  in
-  let url =
-    match xid with
-       Pxp_types.Anonymous          -> raise Pxp_reader.Not_competent
-     | Pxp_types.Public (_,sysname) ->
-        let sysname = resolve sysname in
-         if sysname <> "" then file_url_of_sysname sysname
-                          else raise Pxp_reader.Not_competent
-     | Pxp_types.System sysname     ->
-        let sysname = resolve sysname in
-         file_url_of_sysname sysname
-     | Pxp_types.Private pid -> raise Unexpected
-  in
-  let scheme =
-    try Neturl.url_scheme url with Not_found -> "file" in
-  let host =
-    try Neturl.url_host url with Not_found -> "" in
-    
-  if scheme <> "file" then raise Pxp_reader.Not_competent;
-  if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent;
-    
-  url
-;;
-
-let from_file ?system_encoding utf8_filename =
-  
-  let r =
-    new Pxp_reader.resolve_as_file 
-      ?system_encoding:system_encoding
-      ~url_of_id:file_url_of_id
-      ()
-  in
-
-  let utf8_abs_filename =
-    if utf8_filename <> "" && utf8_filename.[0] = '/' then
-      utf8_filename
-    else
-      Sys.getcwd() ^ "/" ^ utf8_filename
-  in
-
-  let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in
-  let url = Neturl.make_url 
-             ~scheme:"file" 
-             ~host:"localhost" 
-             ~path:(Neturl.split_path utf8_abs_filename) 
-             syntax
-  in
-
-  let xid = Pxp_types.System (Neturl.string_of_url url) in
-    
-
-  Pxp_yacc.ExtID(xid, r)
-;;
-*)
-
-(*PXP 1.1*)
-(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *)
-(* The only reason is to loosen the interface              *)
-
-class resolve_as_file
-  ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec))
-  ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec))
-  ?(system_encoding = `Enc_utf8)
-  ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent))
-  ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent))
-  ()
-  =
-
-  let url_syntax =
-    let enable_if =
-      function
-          `Not_recognized  -> Neturl.Url_part_not_recognized
-        | `Allowed         -> Neturl.Url_part_allowed
-        | `Required        -> Neturl.Url_part_required
-    in
-    { Neturl.null_url_syntax with
-        Neturl.url_enable_scheme = enable_if file_prefix;
-        Neturl.url_enable_host   = enable_if host_prefix;
-        Neturl.url_enable_path   = Neturl.Url_part_required;
-        Neturl.url_accepts_8bits = true;
-    }
-  in
-
-  let base_url_syntax =
-    { Neturl.null_url_syntax with
-        Neturl.url_enable_scheme = Neturl.Url_part_required;
-        Neturl.url_enable_host   = Neturl.Url_part_allowed;
-        Neturl.url_enable_path   = Neturl.Url_part_required;
-        Neturl.url_accepts_8bits = true;
-    }
-  in
-
-  let default_base_url =
-    Neturl.make_url
-      ~scheme: "file"
-      ~host:   ""
-      ~path:   (Neturl.split_path (Sys.getcwd() ^ "/"))
-      base_url_syntax
-  in
-
-  let file_url_of_id xid =
-   let module P = Csc_pxp_reader in
-   let module T = Pxp_types in
-    let file_url_of_sysname sysname =
-      (* By convention, we can assume that sysname is a URL conforming
-       * to RFC 1738 with the exception that it may contain non-ASCII
-       * UTF-8 characters.
-       *)
-      try
-        Neturl.url_of_string url_syntax sysname
-          (* may raise Malformed_URL *)
-      with
-          Neturl.Malformed_URL -> raise P.Not_competent
-    in
-    let url =
-      match xid with
-          T.Anonymous          -> raise P.Not_competent
-        | T.Public (_,sysname) -> let sysname = resolve sysname in
-                                  if sysname <> "" then file_url_of_sysname sysname
-                                                 else raise P.Not_competent
-        | T.System sysname     -> let sysname = resolve sysname in
-                                  file_url_of_sysname sysname
-        | T.Private pid        -> map_private_id pid
-    in
-    let scheme =
-      try Neturl.url_scheme url with Not_found -> "file" in
-    let host =
-      try Neturl.url_host url with Not_found -> "" in
-
-    if scheme <> "file" then raise P.Not_competent;
-    if host <> "" && host <> "localhost" then raise P.Not_competent;
-
-    url
-  in
-
-  let channel_of_file_url xid url =
-   let module P = Csc_pxp_reader in
-   let module T = Pxp_types in
-    match xid with
-        T.Private pid -> open_private_id pid
-      | _ ->
-          ( try
-              let path_utf8 =
-                try Neturl.join_path (Neturl.url_path ~encoded:false url)
-                with Not_found -> raise P.Not_competent
-              in
-
-              let path =
-                Netconversion.recode_string
-                  ~in_enc:  `Enc_utf8
-                  ~out_enc: system_encoding
-                  path_utf8 in
-              (* May raise Malformed_code *)
-
-              open_in_bin path, None
-                (* May raise Sys_error *)
-
-            with
-              | Netconversion.Malformed_code -> assert false
-                (* should not happen *)
-              | Sys_error _ as e ->
-                  raise (P.Not_resolvable e)
-          )
-  in
-
-  Csc_pxp_reader.resolve_read_url_channel
-    ~base_url:       default_base_url
-    ~url_of_id:      file_url_of_id
-    ~channel_of_url: channel_of_file_url
-    ()
-;;
-
-let from_file ?(alt = []) ?system_encoding ?enc utf8_filename =
-  let r =
-    new resolve_as_file
-    ?system_encoding:system_encoding
-      ()
-  in
-                  
-  let url = Csc_pxp_reader.make_file_url
-              ?system_encoding
-              ?enc
-              utf8_filename in
-    
-  let xid = Pxp_types.System (Neturl.string_of_url url) in
-
-  Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt))
-;;
-
diff --git a/helm/metadata/create2/touch/uriManager.ml b/helm/metadata/create2/touch/uriManager.ml
deleted file mode 100644 (file)
index 0fa24cf..0000000
+++ /dev/null
@@ -1,139 +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://cs.unibo.it/helm/.
- *)
-
-(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
-type uri = string array;;
-
-let eq uri1 uri2 =
- uri1 == uri2
-;;
-
-let string_of_uri uri = uri.(Array.length uri - 2);;
-let name_of_uri uri = uri.(Array.length uri - 1);;
-let buri_of_uri uri = uri.(Array.length uri - 3);;
-let depth_of_uri uri = Array.length uri - 2;;
-
-(*CSC: ora e' diventato poco efficiente, migliorare *)
-let relative_depth curi uri cookingsno =
- let rec length_of_current_prefix l1 l2 =
-  match (l1, l2) with
-     (he1::tl1, he2::tl2) when he1 == he2 ->
-       1 + length_of_current_prefix tl1 tl2
-   | (_,_) -> 0
- in
-  depth_of_uri uri -
-   length_of_current_prefix
-    (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno))))
-    (Array.to_list (Array.sub uri 0 (Array.length uri - 2)))
-  (*CSC: vecchio codice da eliminare
-  if eq curi uri then 0
-  else
-   depth_of_uri uri -
-    length_of_current_prefix (Array.to_list curi) (Array.to_list uri)
-  *)
-;;
-
-module OrderedStrings =
- struct
-  type t = string
-  let compare (s1 : t) (s2 : t) = compare s1 s2
- end
-;;
-
-module SetOfStrings = Map.Make(OrderedStrings);;
-
-(*CSC: commento obsoleto ed errato *)
-(* Invariant: the map is the identity function,      *)
-(*  i.e. (SetOfStrings.find str !set_of_uri) == str  *)
-let set_of_uri = ref SetOfStrings.empty;;
-let set_of_prefixes = ref SetOfStrings.empty;;
-
-(* similar to uri_of_string, but used for prefixes of uris *)
-let normalize prefix =
- try
-  SetOfStrings.find prefix !set_of_prefixes
- with
-  Not_found ->
-   set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ;
-   prefix
-;;
-
-exception IllFormedUri of string;;
-
-let mk_prefixes str =
- let rec aux curi =
-  function
-     [he] ->
-      let prefix_uri = curi ^ "/" ^ he
-      and name = List.hd (Str.split (Str.regexp "\.") he) in
-       [ normalize prefix_uri ; name ]
-   | he::tl ->
-      let prefix_uri = curi ^ "/" ^ he in
-       (normalize prefix_uri)::(aux prefix_uri tl)
-   | _ -> raise (IllFormedUri str)
- in
-  let tokens = (Str.split (Str.regexp "/") str) in
-   (* ty = "cic:" *)
-   let (ty, sp) = (List.hd tokens, List.tl tokens) in
-    aux ty sp
-;;
-
-let uri_of_string str =
- try
-  SetOfStrings.find str !set_of_uri
- with
-  Not_found ->
-   let uri = Array.of_list (mk_prefixes str) in
-    set_of_uri := SetOfStrings.add str uri !set_of_uri ;
-    uri
-;;
-
-let cicuri_of_uri uri =
- let completeuri = string_of_uri uri in
-  let newcompleteuri = 
-   (Str.replace_first (Str.regexp "\.types$") ""
-    (Str.replace_first (Str.regexp "\.ann$") "" completeuri))
-  in
-   if completeuri = newcompleteuri then
-    uri
-   else
-    let newuri = Array.copy uri in
-     newuri.(Array.length uri - 2) <- newcompleteuri ;
-     newuri
-;;
-
-let annuri_of_uri uri =
- let completeuri = string_of_uri uri in
-  if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then
-   uri
-  else
-   let newuri = Array.copy uri in
-    newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ;
-    newuri
-;;
-
-let uri_is_annuri uri =
- Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0
-;;
diff --git a/helm/metadata/create2/touch/uriManager.mli b/helm/metadata/create2/touch/uriManager.mli
deleted file mode 100644 (file)
index 2cdd27e..0000000
+++ /dev/null
@@ -1,51 +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://cs.unibo.it/helm/.
- *)
-
-type uri
-
-val eq : uri -> uri -> bool
-
-val uri_of_string : string -> uri
-
-val string_of_uri : uri -> string  (* complete uri *)
-val name_of_uri   : uri -> string  (* name only (without extension)*)
-val buri_of_uri   : uri -> string  (* base uri only *)
-val depth_of_uri  : uri -> int     (* length of the path *)
-
-(* relative_depth curi uri cookingsno                                        *)
-(* is the number of times to cook uri to use it when the current uri is curi *)
-(* cooked cookingsno times                                                   *)
-val relative_depth : uri -> uri -> int -> int
-
-(* given an uri, returns the uri of the corresponding cic file, *)
-(* i.e. removes the [.types][.ann] suffix                       *)
-val cicuri_of_uri : uri -> uri
-
-(* given an uri, returns the uri of the corresponding annotation file, *)
-(* i.e. adds the .ann suffix if not already present                    *)
-val annuri_of_uri : uri -> uri
-
-(* given an uri, tells if it refers to an annotation *)
-val uri_is_annuri : uri -> bool