+++ /dev/null
-(* 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
-;;