]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/test.ml
added mathml_ns
[helm.git] / helm / ocaml / metadata / test.ml
1
2 let _ = Helm_registry.set "getter.mode" "remote";
3 let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
4 let dbd =
5   Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
6     ()
7 in
8 let owner =
9   try
10     Sys.argv.(2)
11   with Invalid_argument _ -> "matita_test"
12 in
13 if Sys.argv.(1) = "clean" then
14   MetadataDb.clean ~dbd ~owner
15 else
16   let uri_str = Sys.argv.(1) in
17   let uri = UriManager.uri_of_string uri_str in
18   match CicEnvironment.get_obj uri with
19   | Cic.Constant (_, body, ty, _) ->
20       MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbd
21   | Cic.InductiveDefinition (types, _, _) ->
22       MetadataDb.index_inductive_def ~dbd ~owner ~uri ~types
23   | _ -> assert false
24