]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/cicParser3.mli
Initial revision
[helm.git] / helm / interface / cicParser3.mli
diff --git a/helm/interface/cicParser3.mli b/helm/interface/cicParser3.mli
new file mode 100644 (file)
index 0000000..dd71ab6
--- /dev/null
@@ -0,0 +1,42 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 24/01/2000                                 *)
+(*                                                                            *)
+(* This module is the terms level of a parser for cic objects from xml        *)
+(* files to the internal representation. It is used by the module cicParser2  *)
+(* (objects level). It defines an extension of the standard dom using the     *)
+(* object-oriented extension machinery of markup: an object with a method     *)
+(* to_cic_term that returns the internal representation of the subtree is     *)
+(* added to each node of the dom tree                                         *)
+(*                                                                            *)
+(******************************************************************************)
+
+exception IllFormedXml of int
+
+val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref
+val current_sp : string list ref
+val current_uri : UriManager.uri ref
+val process_annotations : bool ref
+
+(* the "interface" of the class linked to each node of the dom tree *)
+class virtual cic_term :
+  object ('a)
+
+    (* fields and methods ever required by markup *)
+    val mutable node : cic_term Pxp_document.node option
+    method clone : 'a
+    method node : cic_term Pxp_document.node
+    method set_node : cic_term Pxp_document.node -> unit
+
+    (* a method that returns the internal representation of the tree (term) *)
+    (* rooted in this node                                                  *)
+    method virtual to_cic_term : Cic.annterm
+
+  end
+
+(* The definition of domspec, an hashtable that maps each node type to the *)
+(* object that must be linked to it. Used by markup.                       *)
+val domspec : cic_term Pxp_document.spec