X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2Ftest.ml;fp=helm%2Focaml%2Fmetadata%2Ftest.ml;h=21274a585e37020c4652a1f865439191e8f3b9ed;hb=afb25a74a7c9403c07c67e58efb6460207e228b3;hp=b36ba9176f78369e519f208214ee9e2f444e1256;hpb=c6152ae37c7d2acb6b0f79a50dc64159308b980a;p=helm.git

diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml
index b36ba9176..21274a585 100644
--- a/helm/ocaml/metadata/test.ml
+++ b/helm/ocaml/metadata/test.ml
@@ -10,15 +10,28 @@ let owner =
     Sys.argv.(2)
   with Invalid_argument _ -> "matita_test"
 in
-if Sys.argv.(1) = "clean" then
-  MetadataDb.clean ~dbd ~owner
-else
-  let uri_str = Sys.argv.(1) in
-  let uri = UriManager.uri_of_string uri_str in
-  match CicEnvironment.get_obj uri with
-  | Cic.Constant (_, body, ty, _) ->
-      MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbd
-  | Cic.InductiveDefinition (types, _, _) ->
-      MetadataDb.index_inductive_def ~dbd ~owner ~uri ~types
-  | _ -> assert false
+let _ = MetadataTypes.ownerize_tables owner in
+if Sys.argv.(1) = "clean" then begin
+  prerr_endline "foo";
+  ignore (MetadataDb.clean ~dbd)
+end else
+  let fname = Sys.argv.(1) in
+  let n = ref 0 in
+  let ic = open_in fname in
+  try
+    while true do
+      let line = input_line ic in
+      incr n;
+      Printf.printf "%d\t%s\n" !n line; flush stdout;
+      let uri = UriManager.uri_of_string line in
+      (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+      | Cic.Constant (_, body, ty, _, _), _ ->
+          MetadataDb.index_constant ~body ~ty ~uri ~dbd
+      | Cic.Variable (_, body, ty, _, _), _ ->
+          MetadataDb.index_constant ~body ~ty ~uri ~dbd
+      | Cic.InductiveDefinition (types, _, _, _), _ ->
+          MetadataDb.index_inductive_def ~dbd ~uri ~types
+      | _ -> assert false)
+    done
+  with End_of_file -> close_in ic