]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/annotationParser.ml
This commit was manufactured by cvs2svn to create branch 'helm'.
[helm.git] / helm / interface / annotationParser.ml
diff --git a/helm/interface/annotationParser.ml b/helm/interface/annotationParser.ml
deleted file mode 100644 (file)
index 3c645fe..0000000
+++ /dev/null
@@ -1,30 +0,0 @@
-exception Warnings;;
-
-class warner =
-  object 
-    method warn w =
-      print_endline ("WARNING: " ^ w) ;
-      (raise Warnings : unit)
-  end
-;;
-
-exception EmptyUri;;
-
-let annotate filename ids_to_targets =
- 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
-     AnnotationParser2.annotate ids_to_targets d#root
-  with
-   e ->
-     print_endline (Pxp_types.string_of_exn e) ;
-     raise e
-;;