New procedure to create metadata committed and old procedure removed.

[helm.git] / helm / metadata / create2 / touch / touch.ml

diff --git a/helm/metadata/create2/touch/touch.ml b/helm/metadata/create2/touch/touch.ml
new file mode 100644 (file)
index 0000000..8538a8f
--- /dev/null
+++ b/helm/metadata/create2/touch/touch.ml
@@ -0,0 +1,137 @@
+(* 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 =
+   match CicParser.term_of_xml cicfilename uri false with
+      (annobj, None) ->
+        Deannotate.deannotate_obj annobj
+    | _ -> assert false
+  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
+;;