From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 13 May 2005 13:01:12 +0000 (+0000)
Subject: added list and fill actions
X-Git-Tag: single_binding~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=195cc290eb6e6dc5d5dc9b34bddef083c5c5b0b8;p=helm.git

added list and fill actions
---

diff --git a/helm/ocaml/metadata/table_creator/table_creator.ml b/helm/ocaml/metadata/table_creator/table_creator.ml
index 59289b5df..423edfb27 100644
--- a/helm/ocaml/metadata/table_creator/table_creator.ml
+++ b/helm/ocaml/metadata/table_creator/table_creator.ml
@@ -1,10 +1,12 @@
 
+open Printf
+
 let map =
   (MetadataTypes.library_obj_tbl,`RefObj) ::
   (MetadataTypes.library_sort_tbl,`RefSort) ::
   (MetadataTypes.library_rel_tbl,`RefRel) ::
   (MetadataTypes.library_name_tbl,`ObjectName) ::
-(*  (MetadataTypes.library_???_tbl,`Owners) :: *)
+  (MetadataTypes.library_hits_tbl,`Hits) ::
   (MetadataTypes.library_count_tbl,`Count) :: []
 
 let usage argv_o =
@@ -12,8 +14,10 @@ let usage argv_o =
   prerr_string ("\t" ^ argv_o ^ " what tablename[=rename]\n");
   prerr_string ("\t" ^ argv_o ^ " what all\n\n");
   prerr_endline "what:";
+  prerr_endline "\tlist\tlist table names";
   prerr_endline "\ttable\toutput SQL regarding tables";
-  prerr_endline "\tindex\toutput SQL regarding indexes\n";
+  prerr_endline "\tindex\toutput SQL regarding indexes";
+  prerr_endline "\tfill\toutput SQL filling tables (only \"hits\" supported)\n";
   prerr_string "known tables:\n\t";
   List.iter (fun (n,_) -> prerr_string (" " ^ n)) map;
   prerr_endline "\n"
@@ -37,29 +41,41 @@ let am_i_destructor () =
   
 let main () =
   let len = Array.length Sys.argv in
-  if len < 2 then 
+  if len < 3 then 
     begin
     usage Sys.argv.(0);
     exit 1
     end
   else
     begin
-      let tab,idx =
+      let tab,idx,fill =
         if am_i_destructor () then
-          (SqlStatements.drop_tables,SqlStatements.drop_indexes) 
+          (SqlStatements.drop_tables,SqlStatements.drop_indexes,
+           fun _ t -> [sprintf "DELETE * FROM %s;" t])
         else
-          (SqlStatements.create_tables,SqlStatements.create_indexes)
+          (SqlStatements.create_tables,SqlStatements.create_indexes,
+           SqlStatements.fill_hits)
       in
       let from = 2 in
-      let index = if Sys.argv.(1) = "index" then true else false in
+      let what =
+        match Sys.argv.(1) with
+        | "list" -> `List
+        | "index" -> `Index
+        | "table" -> `Table
+        | "fill" -> `Fill
+        | _ -> failwith "what must be one of \"index\", \"table\", \"fill\""
+      in
       let todo = Array.to_list (Array.sub Sys.argv from (len - from)) in
       let todo = match todo with ["all"] -> List.map fst map | todo -> todo in
       let todo = parse_args todo in
       let todo = List.map (fun (x,name) -> name, (List.assoc x map)) todo in
-      if index then 
-        print_endline (String.concat "\n" (idx todo))
-      else
-        print_endline (String.concat "\n" (tab todo))
+      match what with
+      | `Index -> print_endline (String.concat "\n" (idx todo))
+      | `Table -> print_endline (String.concat "\n" (tab todo))
+      | `Fill ->
+          print_endline (String.concat "\n"
+            (fill MetadataTypes.library_obj_tbl MetadataTypes.library_hits_tbl))
+      | `List -> print_endline (String.concat " " (List.map fst map))
     end
 
 let _ = main ()