]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/cicParser.mli
Initial revision
[helm.git] / helm / interface / cicParser.mli
diff --git a/helm/interface/cicParser.mli b/helm/interface/cicParser.mli
new file mode 100644 (file)
index 0000000..961a262
--- /dev/null
@@ -0,0 +1,19 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 22/03/2000                                 *)
+(*                                                                            *)
+(* This is the main (top level) module of a parser for cic objects from xml   *)
+(* files to the internal representation. It uses the modules cicParser2       *)
+(* (objects level) and cicParser3 (terms level)                               *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* given the filename of an xml file of a cic object and it's uri, it returns *)
+(* its internal annotated representation. The boolean is set to true if the   *)
+(* annotations do really matter                                               *)
+val term_of_xml :
+ string -> UriManager.uri -> bool ->
+  Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option