X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate_V7_mowgli%2Ftouch%2Ftouch.ml;fp=helm%2Fmetadata%2Fcreate_V7_mowgli%2Ftouch%2Ftouch.ml;h=0000000000000000000000000000000000000000;hp=207750a6d815f4ab67fa97303f200b197e18c87c;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8

diff --git a/helm/metadata/create_V7_mowgli/touch/touch.ml b/helm/metadata/create_V7_mowgli/touch/touch.ml
deleted file mode 100644
index 207750a6d..000000000
--- a/helm/metadata/create_V7_mowgli/touch/touch.ml
+++ /dev/null
@@ -1,132 +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>               *)
-(*                                 03/04/2001                                 *)
-(*                                                                            *)
-(*                            Missing description                             *)
-(*                                                                            *)
-(******************************************************************************)
-
-let iteri foo =
- let counter = ref 0 in
-  List.iter (function e -> incr counter ; foo e !counter)
-;;
-
-let pathname_of_uri uristring =
- "backward" ^
-  Str.replace_first (Str.regexp "^cic:") "" uristring
-;;
-
-let make_dirs dirpath =
- ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
-;;
-
-let touch_file rdf_string_uri =
- let module U = UriManager in
-  let rdf_uri = U.uri_of_string rdf_string_uri in
-   make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
-   ignore (
-    Unix.system
-     ("touch \"" ^ (pathname_of_uri rdf_string_uri) ^ "\"")
-   )
-;;
-
-let get_obj uri =
- let cicfilename = Getter.getxml uri in
-  let res = CicParser.obj_of_xml cicfilename None in
-   Unix.unlink cicfilename ;
-   res
-;;
-
-let touch_obj string_uri =
- let module U = UriManager in
- let module C = Cic in
-  function
-     Some (C.InductiveDefinition (itys,_,_)) ->
-      iteri
-       (fun (_,_,_,cons) n ->
-         let sn = string_of_int n in
-          touch_file
-           (string_uri ^ "," ^ sn) ;
-          iteri
-           (fun (_,_) m ->
-             let sm = string_of_int m in
-              touch_file
-               (string_uri ^ "," ^ sn ^ "," ^ sm)
-           ) cons
-       ) itys
-   | Some _ -> assert false
-   | None ->
-      touch_file string_uri
-;;
-
-let touch string_uri =
- let module S = String in
- let module U = UriManager in
-  print_endline ("Now touching metadata file for " ^ string_uri) ;
-  flush stdout ;
-  let uri = U.uri_of_string string_uri in
-  let obj =
-   if S.sub string_uri (S.length string_uri - 3) 3 = "ind" then
-    Some (get_obj uri)
-   else
-    None
-  in
-   touch_obj string_uri obj
-;;
-
-let _ =
- let usage_msg = "usage: touch[.opt] URI" in
- let uri = ref "" in
-  Arg.parse []
-   (fun x ->
-     if x = "" then
-      begin
-       prerr_string "No URI provided.\n" ;
-       Arg.usage [] usage_msg ;
-       exit (-1)
-      end
-     else if !uri = "" then
-      uri := x
-     else
-      begin
-       prerr_string "More than two arguments provided.\n" ;
-       Arg.usage [] usage_msg ;
-       exit (-1)
-      end
-   ) usage_msg ;
-   if !uri = "" then
-    begin
-     prerr_string "No URI provided.\n" ;
-     Arg.usage [] usage_msg ;
-     exit (-1)
-    end ;
-   touch !uri
-;;