X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fpxp%2Fpxp%2Fdoc%2Fmanual%2Fsrc%2Fdtd.mli.ent;fp=helm%2FDEVEL%2Fpxp%2Fpxp%2Fdoc%2Fmanual%2Fsrc%2Fdtd.mli.ent;h=f2e0eb85c48bb9a67b716b5684a80fcdd049b441;hb=c03d2c1fdab8d228cb88aaba5ca0f556318bebc5;hp=0000000000000000000000000000000000000000;hpb=758057e85325f94cd88583feb1fdf6b038e35055;p=helm.git

diff --git a/helm/DEVEL/pxp/pxp/doc/manual/src/dtd.mli.ent b/helm/DEVEL/pxp/pxp/doc/manual/src/dtd.mli.ent
new file mode 100644
index 000000000..f2e0eb85c
--- /dev/null
+++ b/helm/DEVEL/pxp/pxp/doc/manual/src/dtd.mli.ent
@@ -0,0 +1,374 @@
+<!ENTITY markup-dtd1.mli '
+
+(**********************************************************************)
+(*                                                                    *)
+(* Pxp_dtd:                                                           *)
+(*     Object model of document type declarations                     *)
+(*                                                                    *)
+(**********************************************************************)
+
+(* ======================================================================
+ * OVERVIEW
+ *
+ * class dtd ............... represents the whole DTD, including element
+ *                           declarations, entity declarations, notation
+ *                           declarations, and processing instructions
+ * class dtd_element ....... represents an element declaration consisting
+ *                           of a content model and an attribute list
+ *                           declaration
+ * class dtd_notation ...... represents a notation declaration
+ * class proc_instruction .. represents a processing instruction
+ * ======================================================================
+ *
+ *)
+
+
+class dtd :
+  (* Creation:
+   *   new dtd
+   * creates a new, empty DTD object without any declaration, without a root
+   * element, without an ID.
+   *)
+  Pxp_types.collect_warnings -&gt; 
+  Pxp_types.rep_encoding -&gt;
+  object
+    method root : string option
+      (* get the name of the root element if present *)
+
+    method set_root : string -&gt; unit
+      (* set the name of the root element. This method can be invoked 
+       * only once
+       *)
+
+    method id : Pxp_types.dtd_id option
+      (* get the identifier for this DTD *)
+
+    method set_id : Pxp_types.dtd_id -&gt; unit
+      (* set the identifier. This method can be invoked only once *)
+
+    method encoding : Pxp_types.rep_encoding
+      (* returns the encoding used for character representation *)
+
+
+    method allow_arbitrary : unit
+      (* After this method has been invoked, the object changes its behaviour:
+       * - elements and notations that have not been added may be used in an
+       *   arbitrary way; the methods "element" and "notation" indicate this
+       *   by raising Undeclared instead of Validation_error.
+       *)
+
+    method disallow_arbitrary : unit
+
+    method arbitrary_allowed : bool
+      (* Returns whether arbitrary contents are allowed or not. *)
+
+    method standalone_declaration : bool
+      (* Whether there is a &apos;standalone&apos; declaration or not. Strictly 
+       * speaking, this declaration is not part of the DTD, but it is
+       * included here because of practical reasons. 
+       * If not set, this property defaults to &apos;false&apos;.
+       *)
+
+    method set_standalone_declaration : bool -&gt; unit
+      (* Sets the &apos;standalone&apos; declaration. *)
+
+
+    method add_element : dtd_element -&gt; unit
+      (* add the given element declaration to this DTD. Raises Not_found
+       * if there is already an element declaration with the same name.
+       *)
+
+    method add_gen_entity : Pxp_entity.entity -&gt; bool -&gt; unit
+      (* add_gen_entity e extdecl:
+       * add the entity &apos;e&apos; as general entity to this DTD (general entities
+       * are those represented by &amp;name;). If there is already a declaration
+       * with the same name, the second definition is ignored; as exception from
+       * this rule, entities with names "lt", "gt", "amp", "quot", and "apos"
+       * may only be redeclared with a definition that is equivalent to the
+       * standard definition; otherwise a Validation_error is raised.
+       *
+       * &apos;extdecl&apos;: &apos;true&apos; indicates that the entity declaration occurs in
+       * an external entity. (Used for the standalone check.)
+       *)
+
+    method add_par_entity : Pxp_entity.entity -&gt; unit
+      (* add the given entity as parameter entity to this DTD (parameter
+       * entities are those represented by &percent;name;). If there is already a 
+       * declaration with the same name, the second definition is ignored.
+       *)
+
+    method add_notation : dtd_notation -&gt; unit
+      (* add the given notation to this DTD. If there is already a declaration
+       * with the same name, a Validation_error is raised.
+       *)
+
+    method add_pinstr : proc_instruction -&gt; unit
+      (* add the given processing instruction to this DTD. *)
+
+    method element : string -&gt; dtd_element
+      (* looks up the element declaration with the given name. Raises 
+       * Validation_error if the element cannot be found. (If "allow_arbitrary"
+       * has been invoked before, Unrestricted is raised instead.)
+       *)
+
+    method element_names : string list
+      (* returns the list of the names of all element declarations. *)
+
+    method gen_entity : string -&gt; (Pxp_entity.entity * bool)
+      (* let e, extdecl = obj # gen_entity n:
+       * looks up the general entity &apos;e&apos; with the name &apos;n&apos;. Raises
+       * WF_error if the entity cannot be found.
+       * &apos;extdecl&apos;: indicates whether the entity declaration occured in an 
+       * external entity.
+       *)
+
+    method gen_entity_names : string list
+      (* returns the list of all general entity names *)
+
+    method par_entity : string -&gt; Pxp_entity.entity
+      (* looks up the parameter entity with the given name. Raises
+       * WF_error if the entity cannot be found.
+       *)
+
+    method par_entity_names : string list
+      (* returns the list of all parameter entity names *)
+
+    method notation : string -&gt; dtd_notation
+      (* looks up the notation declaration with the given name. Raises
+       * Validation_error if the notation cannot be found. (If "allow_arbitrary"
+       * has been invoked before, Unrestricted is raised instead.)
+       *)
+
+    method notation_names : string list
+      (* Returns the list of the names of all added notations *)
+
+    method pinstr : string -&gt; proc_instruction list
+      (* looks up all processing instructions with the given target.
+       * The "target" is the identifier following "&lt;?".
+       * Note: It is not possible to find out the exact position of the
+       * processing instruction.
+       *)
+
+    method pinstr_names : string list
+      (* Returns the list of the names (targets) of all added pinstrs *)
+
+    method validate : unit
+      (* ensures that the DTD is valid. This method is optimized such that
+       * actual validation is only performed if DTD has changed.
+       * If the DTD is invalid, mostly a Validation_error is raised,
+       * but other exceptions are possible, too.
+       *)
+
+    method only_deterministic_models : unit
+      (* Succeeds if all regexp content models are deterministic. 
+       * Otherwise Validation_error.
+       *)
+
+    method write : Pxp_types.output_stream -&gt; Pxp_types.encoding -&gt; bool -&gt; unit
+      (* write_compact_as_latin1 os enc doctype:
+       * Writes the DTD as &apos;enc&apos;-encoded string to &apos;os&apos;. If &apos;doctype&apos;, a 
+       * DTD like &lt;!DOCTYPE root [ ... ]&gt; is written. If &apos;not doctype&apos;,
+       * only the declarations are written (the material within the
+       * square brackets).
+       *)
+
+    method write_compact_as_latin1 : Pxp_types.output_stream -&gt; bool -&gt; unit
+      (* DEPRECATED METHOD; included only to keep compatibility with
+       * older versions of the parser
+       *)
+
+
+    (*----------------------------------------*)
+    method invalidate : unit
+      (* INTERNAL METHOD *)
+    method warner : Pxp_types.collect_warnings
+      (* INTERNAL METHOD *)
+  end
+
+'>
+<!ENTITY markup-dtd2.mli '
+
+(* ---------------------------------------------------------------------- *)
+
+and dtd_element : dtd -&gt; string -&gt; 
+  (* Creation:
+   *   new dtd_element init_dtd init_name:
+   * creates a new dtd_element object for init_dtd with init_name.
+   * The strings are represented in the same encoding as init_dtd.
+   *)
+  object
+
+    method name : string
+      (* returns the name of the declared element *)
+
+    method externally_declared : bool
+      (* returns whether the element declaration occurs in an external
+       * entity.
+       *)
+
+    method content_model : Pxp_types.content_model_type
+      (* get the content model of this element declaration, or Unspecified *)
+
+    method content_dfa : Pxp_dfa.dfa_definition option
+      (* return the DFA of the content model if there is a DFA, or None.
+       * A DFA exists only for regexp style content models which are
+       * deterministic.
+       *)
+
+    method set_cm_and_extdecl : Pxp_types.content_model_type -&gt; bool -&gt; unit
+      (* set_cm_and_extdecl cm extdecl:
+       * set the content model to &apos;cm&apos;. Once the content model is not 
+       * Unspecified, it cannot be set to a different value again.
+       * Furthermore, it is set whether the element occurs in an external
+       * entity (&apos;extdecl&apos;).
+       *)
+
+    method encoding : Pxp_types.rep_encoding
+      (* Return the encoding of the strings *)
+
+    method allow_arbitrary : unit
+      (* After this method has been invoked, the object changes its behaviour:
+       * - attributes that have not been added may be used in an
+       *   arbitrary way; the method "attribute" indicates this
+       *   by raising Undeclared instead of Validation_error.
+       *)
+
+    method disallow_arbitrary : unit
+
+    method arbitrary_allowed : bool
+      (* Returns whether arbitrary attributes are allowed or not. *)
+
+    method attribute : string -&gt; 
+                         Pxp_types.att_type * Pxp_types.att_default
+      (* get the type and default value of a declared attribute, or raise
+       * Validation_error if the attribute does not exist.
+       * If &apos;arbitrary_allowed&apos;, the exception Undeclared is raised instead
+       * of Validation_error.
+       *)
+
+    method attribute_violates_standalone_declaration : 
+               string -&gt; string option -&gt; bool
+      (* attribute_violates_standalone_declaration name v:
+       * Checks whether the attribute &apos;name&apos; violates the "standalone"
+       * declaration if it has value &apos;v&apos;.
+       * The method returns true if:
+       * - The attribute declaration occurs in an external entity, 
+       * and if one of the two conditions holds:
+       * - v = None, and there is a default for the attribute value
+       * - v = Some s, and the type of the attribute is not CDATA,
+       *   and s changes if normalized according to the rules of the
+       *   attribute type.
+       *
+       * The method raises Validation_error if the attribute does not exist.
+       * If &apos;arbitrary_allowed&apos;, the exception Undeclared is raised instead
+       * of Validation_error.
+       *)
+
+    method attribute_names : string list
+      (* get the list of all declared attributes *)
+
+    method names_of_required_attributes : string list
+      (* get the list of all attributes that are specified as required 
+       * attributes
+       *)
+
+    method id_attribute_name : string option
+      (* Returns the name of the attribute with type ID, or None. *)
+
+    method idref_attribute_names : string list
+      (* Returns the names of the attributes with type IDREF or IDREFS. *)
+
+    method add_attribute : string -&gt; 
+                           Pxp_types.att_type -&gt; 
+			   Pxp_types.att_default -&gt; 
+			   bool -&gt;
+			     unit
+      (* add_attribute name type default extdecl:
+       * add an attribute declaration for an attribute with the given name,
+       * type, and default value. If there is more than one declaration for
+       * an attribute name, the first declaration counts; the other declarations
+       * are ignored.
+       * &apos;extdecl&apos;: if true, the attribute declaration occurs in an external
+       * entity. This property is used to check the "standalone" attribute.
+       *)
+
+    method validate : unit
+      (* checks whether this element declaration (i.e. the content model and
+       * all attribute declarations) is valid for the associated DTD.
+       * Raises mostly Validation_error if the validation fails.
+       *)
+
+    method write : Pxp_types.output_stream -&gt; Pxp_types.encoding -&gt; unit
+      (* write_compact_as_latin1 os enc:
+       * Writes the &lt;!ELEMENT ... &gt; declaration to &apos;os&apos; as &apos;enc&apos;-encoded string.
+       *)
+
+    method write_compact_as_latin1 : Pxp_types.output_stream -&gt; unit
+      (* DEPRECATED METHOD; included only to keep compatibility with
+       * older versions of the parser
+       *)
+  end
+
+(* ---------------------------------------------------------------------- *)
+
+and dtd_notation : string -&gt; Pxp_types.ext_id -&gt; Pxp_types.rep_encoding -&gt;
+  (* Creation:
+   *    new dtd_notation a_name an_external_ID init_encoding
+   * creates a new dtd_notation object with the given name and the given
+   * external ID.
+   *)
+  object
+    method name : string
+    method ext_id : Pxp_types.ext_id
+    method encoding : Pxp_types.rep_encoding
+
+    method write : Pxp_types.output_stream -&gt; Pxp_types.encoding -&gt; unit
+      (* write_compact_as_latin1 os enc:
+       * Writes the &lt;!NOTATION ... &gt; declaration to &apos;os&apos; as &apos;enc&apos;-encoded 
+       * string.
+       *)
+
+    method write_compact_as_latin1 : Pxp_types.output_stream -&gt; unit
+      (* DEPRECATED METHOD; included only to keep compatibility with
+       * older versions of the parser
+       *)
+
+  end
+
+(* ---------------------------------------------------------------------- *)
+
+and proc_instruction : string -&gt; string -&gt; Pxp_types.rep_encoding -&gt;
+  (* Creation:
+   *   new proc_instruction a_target a_value
+   * creates a new proc_instruction object with the given target string and
+   * the given value string. 
+   * Note: A processing instruction is written as &lt;?target value?&gt;. 
+   *)
+  object
+    method target : string
+    method value : string
+    method encoding : Pxp_types.rep_encoding
+
+    method write : Pxp_types.output_stream -&gt; Pxp_types.encoding -&gt; unit
+      (* write os enc:
+       * Writes the &lt;?...?&gt; PI to &apos;os&apos; as &apos;enc&apos;-encoded string.
+       *)
+
+    method write_compact_as_latin1 : Pxp_types.output_stream -&gt; unit
+      (* DEPRECATED METHOD; included only to keep compatibility with
+       * older versions of the parser
+       *)
+
+    method parse_pxp_option : (string * string * (string * string) list)
+      (* Parses a PI containing a PXP option. Such PIs are formed like:
+       *   &lt;?target option-name option-att="value" option-att="value" ... ?&gt;
+       * The method returns a triple
+       *   (target, option-name, [option-att, value; ...])
+       * or raises Error.
+       *)
+
+  end
+
+;;
+
+'>