]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicParser3.mli
dd71ab6eae38b4dcd217809088072a693c4361b6
[helm.git] / helm / interface / cicParser3.mli
1 (******************************************************************************)
2 (*                                                                            *)
3 (*                               PROJECT HELM                                 *)
4 (*                                                                            *)
5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
6 (*                                 24/01/2000                                 *)
7 (*                                                                            *)
8 (* This module is the terms level of a parser for cic objects from xml        *)
9 (* files to the internal representation. It is used by the module cicParser2  *)
10 (* (objects level). It defines an extension of the standard dom using the     *)
11 (* object-oriented extension machinery of markup: an object with a method     *)
12 (* to_cic_term that returns the internal representation of the subtree is     *)
13 (* added to each node of the dom tree                                         *)
14 (*                                                                            *)
15 (******************************************************************************)
16
17 exception IllFormedXml of int
18
19 val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref
20 val current_sp : string list ref
21 val current_uri : UriManager.uri ref
22 val process_annotations : bool ref
23
24 (* the "interface" of the class linked to each node of the dom tree *)
25 class virtual cic_term :
26   object ('a)
27
28     (* fields and methods ever required by markup *)
29     val mutable node : cic_term Pxp_document.node option
30     method clone : 'a
31     method node : cic_term Pxp_document.node
32     method set_node : cic_term Pxp_document.node -> unit
33
34     (* a method that returns the internal representation of the tree (term) *)
35     (* rooted in this node                                                  *)
36     method virtual to_cic_term : Cic.annterm
37
38   end
39
40 (* The definition of domspec, an hashtable that maps each node type to the *)
41 (* object that must be linked to it. Used by markup.                       *)
42 val domspec : cic_term Pxp_document.spec