X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FtheoryParser.ml;fp=helm%2Finterface%2FtheoryParser.ml;h=abc3528074578654bc5ff917679beec6fcbaf77d;hb=c01d2aaea05f7385bee46addd900cd0397756389;hp=0000000000000000000000000000000000000000;hpb=38e1ee1df7be76922343935255e26673af8c7682;p=helm.git

diff --git a/helm/interface/theoryParser.ml b/helm/interface/theoryParser.ml
new file mode 100644
index 000000000..abc352807
--- /dev/null
+++ b/helm/interface/theoryParser.ml
@@ -0,0 +1,29 @@
+exception Warnings;;
+
+class warner =
+  object 
+    method warn w =
+      print_endline ("WARNING: " ^ w) ;
+      (raise Warnings : unit)
+  end
+;;
+
+exception EmptyUri;;
+
+let theory_of_xml filename =
+ let module Y = Pxp_yacc in
+  try 
+    let d =
+     let config = {Y.default_config with Y.warner = new warner} in
+      Y.parse_document_entity config
+(*PXP       (Y.ExtID (Pxp_types.System filename,
+         new Pxp_reader.resolve_as_file ~url_of_id ()))
+*)     (PxpUriResolver.from_file filename)
+       Y.default_spec
+    in
+     TheoryParser2.get_theory d#root
+  with
+   e ->
+     print_endline (Pxp_types.string_of_exn e) ;
+     raise e
+;;