1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* Missing description *)
35 (******************************************************************************)
38 let counter = ref 0 in
39 List.iter (function e -> incr counter ; foo e !counter)
42 let pathname_of_uri uristring =
44 Str.replace_first (Str.regexp "^cic:") "" uristring
47 let make_dirs dirpath =
48 ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
51 let touch_file rdf_string_uri =
52 let module U = UriManager in
53 let rdf_uri = U.uri_of_string rdf_string_uri in
54 make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
57 ("touch \"" ^ (pathname_of_uri rdf_string_uri) ^ "\"")
62 let cicfilename = Getter.getxml uri in
64 match CicParser.term_of_xml cicfilename uri false with
66 Deannotate.deannotate_obj annobj
69 Unix.unlink cicfilename ;
73 let touch_obj string_uri =
74 let module U = UriManager in
77 Some (C.InductiveDefinition (itys,_,_)) ->
79 (fun (_,_,_,cons) n ->
80 let sn = string_of_int n in
82 (string_uri ^ "," ^ sn) ;
85 let sm = string_of_int m in
87 (string_uri ^ "," ^ sn ^ "," ^ sm)
90 | Some _ -> assert false
95 let touch string_uri =
96 let module S = String in
97 let module U = UriManager in
98 print_endline ("Now touching metadata file for " ^ string_uri) ;
100 let uri = U.uri_of_string string_uri in
102 if S.sub string_uri (S.length string_uri - 3) 3 = "ind" then
107 touch_obj string_uri obj
111 let usage_msg = "usage: touch[.opt] URI" in
117 prerr_string "No URI provided.\n" ;
118 Arg.usage [] usage_msg ;
121 else if !uri = "" then
125 prerr_string "More than two arguments provided.\n" ;
126 Arg.usage [] usage_msg ;
132 prerr_string "No URI provided.\n" ;
133 Arg.usage [] usage_msg ;