]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/pxp/pxp/doc/manual/html/x1629.html
This commit was manufactured by cvs2svn to create branch 'init'.
[helm.git] / helm / DEVEL / pxp / pxp / doc / manual / html / x1629.html
diff --git a/helm/DEVEL/pxp/pxp/doc/manual/html/x1629.html b/helm/DEVEL/pxp/pxp/doc/manual/html/x1629.html
deleted file mode 100644 (file)
index 06b1e60..0000000
+++ /dev/null
@@ -1,895 +0,0 @@
-<HTML
-><HEAD
-><TITLE
->Resolvers and sources</TITLE
-><META
-NAME="GENERATOR"
-CONTENT="Modular DocBook HTML Stylesheet Version 1.46"><LINK
-REL="HOME"
-TITLE="The PXP user's guide"
-HREF="index.html"><LINK
-REL="UP"
-TITLE="Configuring and calling the parser"
-HREF="c1567.html"><LINK
-REL="PREVIOUS"
-TITLE="Configuring and calling the parser"
-HREF="c1567.html"><LINK
-REL="NEXT"
-TITLE="The DTD classes"
-HREF="x1812.html"><LINK
-REL="STYLESHEET"
-TYPE="text/css"
-HREF="markup.css"></HEAD
-><BODY
-CLASS="SECT1"
-BGCOLOR="#FFFFFF"
-TEXT="#000000"
-LINK="#0000FF"
-VLINK="#840084"
-ALINK="#0000FF"
-><DIV
-CLASS="NAVHEADER"
-><TABLE
-WIDTH="100%"
-BORDER="0"
-CELLPADDING="0"
-CELLSPACING="0"
-><TR
-><TH
-COLSPAN="3"
-ALIGN="center"
->The PXP user's guide</TH
-></TR
-><TR
-><TD
-WIDTH="10%"
-ALIGN="left"
-VALIGN="bottom"
-><A
-HREF="c1567.html"
->Prev</A
-></TD
-><TD
-WIDTH="80%"
-ALIGN="center"
-VALIGN="bottom"
->Chapter 4. Configuring and calling the parser</TD
-><TD
-WIDTH="10%"
-ALIGN="right"
-VALIGN="bottom"
-><A
-HREF="x1812.html"
->Next</A
-></TD
-></TR
-></TABLE
-><HR
-ALIGN="LEFT"
-WIDTH="100%"></DIV
-><DIV
-CLASS="SECT1"
-><H1
-CLASS="SECT1"
-><A
-NAME="AEN1629"
->4.2. Resolvers and sources</A
-></H1
-><DIV
-CLASS="SECT2"
-><H2
-CLASS="SECT2"
-><A
-NAME="AEN1631"
->4.2.1. Using the built-in resolvers (called sources)</A
-></H2
-><P
->The type <TT
-CLASS="LITERAL"
->source</TT
-> enumerates the two
-possibilities where the document to parse comes from.
-
-<PRE
-CLASS="PROGRAMLISTING"
->type source =
-    Entity of ((dtd -&gt; Pxp_entity.entity) * Pxp_reader.resolver)
-  | ExtID of (ext_id * Pxp_reader.resolver)</PRE
->
-
-You normally need not to worry about this type as there are convenience
-functions that create <TT
-CLASS="LITERAL"
->source</TT
-> values:
-
-
-            <P
-></P
-><UL
-COMPACT="COMPACT"
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->from_file s</TT
->: The document is read from
-file <TT
-CLASS="LITERAL"
->s</TT
->; you may specify absolute or relative path names.
-The file name must be encoded as UTF-8 string.</P
-><P
->There is an optional argument <TT
-CLASS="LITERAL"
->~system_encoding</TT
->
-specifying the character encoding which is used for the names of the file
-system. For example, if this encoding is ISO-8859-1 and <TT
-CLASS="LITERAL"
->s</TT
-> is
-also a ISO-8859-1 string, you can form the source:
-
-<PRE
-CLASS="PROGRAMLISTING"
->let s_utf8  =  recode_string ~in_enc:`Enc_iso88591 ~out_enc:`Enc_utf8 s in
-from_file ~system_encoding:`Enc_iso88591 s_utf8</PRE
-></P
-><P
->This <TT
-CLASS="LITERAL"
->source</TT
-> has the advantage that
-it is able to resolve inner external entities; i.e. if your document includes
-data from another file (using the <TT
-CLASS="LITERAL"
->SYSTEM</TT
-> attribute), this
-mode will find that file. However, this mode cannot resolve
-<TT
-CLASS="LITERAL"
->PUBLIC</TT
-> identifiers nor <TT
-CLASS="LITERAL"
->SYSTEM</TT
-> identifiers
-other than "file:".</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->from_channel ch</TT
->: The document is read
-from the channel <TT
-CLASS="LITERAL"
->ch</TT
->. In general, this source also supports
-file URLs found in the document; however, by default only absolute URLs are
-understood. It is possible to associate an ID with the channel such that the
-resolver knows how to interpret relative URLs:
-
-<PRE
-CLASS="PROGRAMLISTING"
->from_channel ~id:(System "file:///dir/dir1/") ch</PRE
->
-
-There is also the ~system_encoding argument specifying how file names are
-encoded. - The example from above can also be written (but it is no
-longer possible to interpret relative URLs because there is no ~id argument,
-and computing this argument is relatively complicated because it must
-be a valid URL):
-
-<PRE
-CLASS="PROGRAMLISTING"
->let ch = open_in s in
-let src = from_channel ~system_encoding:`Enc_iso88591 ch in
-...;
-close_in ch</PRE
-></P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->from_string s</TT
->: The string
-<TT
-CLASS="LITERAL"
->s</TT
-> is the document to parse. This mode is not able to
-interpret file names of <TT
-CLASS="LITERAL"
->SYSTEM</TT
-> clauses, nor it can look up
-<TT
-CLASS="LITERAL"
->PUBLIC</TT
-> identifiers. </P
-><P
->Normally, the encoding of the string is detected as usual
-by analyzing the XML declaration, if any. However, it is also possible to
-specify the encoding directly:
-
-<PRE
-CLASS="PROGRAMLISTING"
->let src = from_string ~fixenc:`ISO-8859-2 s</PRE
-></P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->ExtID (id, r)</TT
->: The document to parse
-is denoted by the identifier <TT
-CLASS="LITERAL"
->id</TT
-> (either a
-<TT
-CLASS="LITERAL"
->SYSTEM</TT
-> or <TT
-CLASS="LITERAL"
->PUBLIC</TT
-> clause), and this
-identifier is interpreted by the resolver <TT
-CLASS="LITERAL"
->r</TT
->. Use this mode
-if you have written your own resolver.</P
-><P
->Which character sets are possible depends on the passed
-resolver <TT
-CLASS="LITERAL"
->r</TT
->.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->Entity (get_entity, r)</TT
->: The document
-to parse is returned by the function invocation <TT
-CLASS="LITERAL"
->get_entity
-dtd</TT
->, where <TT
-CLASS="LITERAL"
->dtd</TT
-> is the DTD object to use (it may be
-empty). Inner external references occuring in this entity are resolved using
-the resolver <TT
-CLASS="LITERAL"
->r</TT
->.</P
-><P
->Which character sets are possible depends on the passed
-resolver <TT
-CLASS="LITERAL"
->r</TT
->.</P
-></LI
-></UL
-></P
-></DIV
-><DIV
-CLASS="SECT2"
-><H2
-CLASS="SECT2"
-><A
-NAME="AEN1682"
->4.2.2. The resolver API</A
-></H2
-><P
->A resolver is an object that can be opened like a file, but you
-do not pass the file name to the resolver, but the XML identifier of the entity
-to read from (either a <TT
-CLASS="LITERAL"
->SYSTEM</TT
-> or <TT
-CLASS="LITERAL"
->PUBLIC</TT
->
-clause). When opened, the resolver must return the
-<TT
-CLASS="LITERAL"
->Lexing.lexbuf</TT
-> that reads the characters.  The resolver can
-be closed, and it can be cloned. Furthermore, it is possible to tell the
-resolver which character set it should assume. - The following from Pxp_reader:
-
-<PRE
-CLASS="PROGRAMLISTING"
->exception Not_competent
-exception Not_resolvable of exn
-
-class type resolver =
-  object
-    method init_rep_encoding : rep_encoding -&#62; unit
-    method init_warner : collect_warnings -&#62; unit
-    method rep_encoding : rep_encoding
-    method open_in : ext_id -&#62; Lexing.lexbuf
-    method close_in : unit
-    method change_encoding : string -&#62; unit
-    method clone : resolver
-    method close_all : unit
-  end</PRE
->
-
-The resolver object must work as follows:</P
-><P
->            <P
-></P
-><UL
-COMPACT="COMPACT"
-><LI
-STYLE="list-style-type: disc"
-><P
->When the parser is called, it tells the resolver the
-warner object and the internal encoding by invoking
-<TT
-CLASS="LITERAL"
->init_warner</TT
-> and <TT
-CLASS="LITERAL"
->init_rep_encoding</TT
->. The
-resolver should store these values. The method <TT
-CLASS="LITERAL"
->rep_encoding</TT
->
-should return the internal encoding.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If the parser wants to read from the resolver, it invokes
-the method <TT
-CLASS="LITERAL"
->open_in</TT
->. Either the resolver succeeds, in which
-case the <TT
-CLASS="LITERAL"
->Lexing.lexbuf</TT
-> reading from the file or stream must
-be returned, or opening fails. In the latter case the method implementation
-should raise an exception (see below).</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If the parser finishes reading, it calls the
-<TT
-CLASS="LITERAL"
->close_in</TT
-> method.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If the parser finds a reference to another external
-entity in the input stream, it calls <TT
-CLASS="LITERAL"
->clone</TT
-> to get a second
-resolver which must be initially closed (not yet connected with an input
-stream).  The parser then invokes <TT
-CLASS="LITERAL"
->open_in</TT
-> and the other
-methods as described.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If you already know the character set of the input
-stream, you should recode it to the internal encoding, and define the method
-<TT
-CLASS="LITERAL"
->change_encoding</TT
-> as an empty method.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If you want to support multiple external character sets,
-the object must follow a much more complicated protocol. Directly after
-<TT
-CLASS="LITERAL"
->open_in</TT
-> has been called, the resolver must return a lexical
-buffer that only reads one byte at a time. This is only possible if you create
-the lexical buffer with <TT
-CLASS="LITERAL"
->Lexing.from_function</TT
->; the function
-must then always return 1 if the EOF is not yet reached, and 0 if EOF is
-reached. If the parser has read the first line of the document, it will invoke
-<TT
-CLASS="LITERAL"
->change_encoding</TT
-> to tell the resolver which character set to
-assume. From this moment, the object can return more than one byte at once. The
-argument of <TT
-CLASS="LITERAL"
->change_encoding</TT
-> is either the parameter of the
-"encoding" attribute of the XML declaration, or the empty string if there is
-not any XML declaration or if the declaration does not contain an encoding
-attribute. </P
-><P
->At the beginning the resolver must only return one
-character every time something is read from the lexical buffer. The reason for
-this is that you otherwise would not exactly know at which position in the
-input stream the character set changes.</P
-><P
->If you want automatic recognition of the character set,
-it is up to the resolver object to implement this.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
->If an error occurs, the parser calls the method
-<TT
-CLASS="LITERAL"
->close_all</TT
-> for the top-level resolver; this method should
-close itself (if not already done) and all clones.</P
-></LI
-></UL
-></P
-><DIV
-CLASS="FORMALPARA"
-><P
-><B
->Exceptions. </B
->It is possible to chain resolvers such that when the first resolver is not able
-to open the entity, the other resolvers of the chain are tried in turn. The
-method <TT
-CLASS="LITERAL"
->open_in</TT
-> should raise the exception
-<TT
-CLASS="LITERAL"
->Not_competent</TT
-> to indicate that the next resolver should try
-to open the entity. If the resolver is able to handle the ID, but some other
-error occurs, the exception <TT
-CLASS="LITERAL"
->Not_resolvable</TT
-> should be raised
-to force that the chain breaks.
-         </P
-></DIV
-><P
->Example: How to define a resolver that is equivalent to
-from_string: ...</P
-></DIV
-><DIV
-CLASS="SECT2"
-><H2
-CLASS="SECT2"
-><A
-NAME="AEN1728"
->4.2.3. Predefined resolver components</A
-></H2
-><P
->There are some classes in Pxp_reader that define common resolver behaviour.
-
-<PRE
-CLASS="PROGRAMLISTING"
->class resolve_read_this_channel : 
-    ?id:ext_id -&#62; 
-    ?fixenc:encoding -&#62; 
-    ?auto_close:bool -&#62; 
-    in_channel -&#62; 
-        resolver</PRE
->
-
-Reads from the passed channel (it may be even a pipe). If the
-<TT
-CLASS="LITERAL"
->~id</TT
-> argument is passed to the object, the created resolver
-accepts only this ID. Otherwise all IDs are accepted.  - Once the resolver has
-been cloned, it does not accept any ID. This means that this resolver cannot
-handle inner references to external entities. Note that you can combine this
-resolver with another resolver that can handle inner references (such as
-resolve_as_file); see class 'combine' below.  - If you pass the
-<TT
-CLASS="LITERAL"
->~fixenc</TT
-> argument, the encoding of the channel is set to the
-passed value, regardless of any auto-recognition or any XML declaration. - If
-<TT
-CLASS="LITERAL"
->~auto_close = true</TT
-> (which is the default), the channel is
-closed after use. If <TT
-CLASS="LITERAL"
->~auto_close = false</TT
->, the channel is
-left open.
- </P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class resolve_read_any_channel : 
-    ?auto_close:bool -&#62; 
-    channel_of_id:(ext_id -&#62; (in_channel * encoding option)) -&#62; 
-        resolver</PRE
->
-
-This resolver calls the function <TT
-CLASS="LITERAL"
->~channel_of_id</TT
-> to open a
-new channel for the passed <TT
-CLASS="LITERAL"
->ext_id</TT
->. This function must either
-return the channel and the encoding, or it must fail with Not_competent.  The
-function must return <TT
-CLASS="LITERAL"
->None</TT
-> as encoding if the default
-mechanism to recognize the encoding should be used. It must return
-<TT
-CLASS="LITERAL"
->Some e</TT
-> if it is already known that the encoding of the
-channel is <TT
-CLASS="LITERAL"
->e</TT
->.  If <TT
-CLASS="LITERAL"
->~auto_close = true</TT
->
-(which is the default), the channel is closed after use. If
-<TT
-CLASS="LITERAL"
->~auto_close = false</TT
->, the channel is left open.</P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class resolve_read_url_channel :
-    ?base_url:Neturl.url -&#62;
-    ?auto_close:bool -&#62; 
-    url_of_id:(ext_id -&#62; Neturl.url) -&#62; 
-    channel_of_url:(Neturl.url -&#62; (in_channel * encoding option)) -&#62; 
-        resolver</PRE
->
-
-When this resolver gets an ID to read from, it calls the function
-<TT
-CLASS="LITERAL"
->~url_of_id</TT
-> to get the corresponding URL. This URL may be a
-relative URL; however, a URL scheme must be used which contains a path.  The
-resolver converts the URL to an absolute URL if necessary.  The second
-function, <TT
-CLASS="LITERAL"
->~channel_of_url</TT
->, is fed with the absolute URL as
-input. This function opens the resource to read from, and returns the channel
-and the encoding of the resource.</P
-><P
->Both functions, <TT
-CLASS="LITERAL"
->~url_of_id</TT
-> and
-<TT
-CLASS="LITERAL"
->~channel_of_url</TT
->, can raise Not_competent to indicate that
-the object is not able to read from the specified resource. However, there is a
-difference: A Not_competent from <TT
-CLASS="LITERAL"
->~url_of_id</TT
-> is left as it
-is, but a Not_competent from <TT
-CLASS="LITERAL"
->~channel_of_url</TT
-> is converted to
-Not_resolvable. So only <TT
-CLASS="LITERAL"
->~url_of_id</TT
-> decides which URLs are
-accepted by the resolver and which not.</P
-><P
->The function <TT
-CLASS="LITERAL"
->~channel_of_url</TT
-> must return
-<TT
-CLASS="LITERAL"
->None</TT
-> as encoding if the default mechanism to recognize the
-encoding should be used. It must return <TT
-CLASS="LITERAL"
->Some e</TT
-> if it is
-already known that the encoding of the channel is <TT
-CLASS="LITERAL"
->e</TT
->.</P
-><P
->If <TT
-CLASS="LITERAL"
->~auto_close = true</TT
-> (which is the default), the channel is
-closed after use. If <TT
-CLASS="LITERAL"
->~auto_close = false</TT
->, the channel is
-left open.</P
-><P
->Objects of this class contain a base URL relative to which relative URLs are
-interpreted. When creating a new object, you can specify the base URL by
-passing it as <TT
-CLASS="LITERAL"
->~base_url</TT
-> argument. When an existing object is
-cloned, the base URL of the clone is the URL of the original object. - Note
-that the term "base URL" has a strict definition in RFC 1808.</P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class resolve_read_this_string : 
-    ?id:ext_id -&#62; 
-    ?fixenc:encoding -&#62; 
-    string -&#62; 
-        resolver</PRE
->
-
-Reads from the passed string. If the <TT
-CLASS="LITERAL"
->~id</TT
-> argument is passed
-to the object, the created resolver accepts only this ID. Otherwise all IDs are
-accepted. - Once the resolver has been cloned, it does not accept any ID. This
-means that this resolver cannot handle inner references to external
-entities. Note that you can combine this resolver with another resolver that
-can handle inner references (such as resolve_as_file); see class 'combine'
-below. - If you pass the <TT
-CLASS="LITERAL"
->~fixenc</TT
-> argument, the encoding of
-the string is set to the passed value, regardless of any auto-recognition or
-any XML declaration.</P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class resolve_read_any_string : 
-    string_of_id:(ext_id -&#62; (string * encoding option)) -&#62; 
-        resolver</PRE
->
-
-This resolver calls the function <TT
-CLASS="LITERAL"
->~string_of_id</TT
-> to get the
-string for the passed <TT
-CLASS="LITERAL"
->ext_id</TT
->. This function must either
-return the string and the encoding, or it must fail with Not_competent.  The
-function must return <TT
-CLASS="LITERAL"
->None</TT
-> as encoding if the default
-mechanism to recognize the encoding should be used. It must return
-<TT
-CLASS="LITERAL"
->Some e</TT
-> if it is already known that the encoding of the
-string is <TT
-CLASS="LITERAL"
->e</TT
->.</P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class resolve_as_file :
-    ?file_prefix:[ `Not_recognized | `Allowed | `Required ] -&#62;
-    ?host_prefix:[ `Not_recognized | `Allowed | `Required ] -&#62;
-    ?system_encoding:encoding -&#62;
-    ?url_of_id:(ext_id -&#62; Neturl.url) -&#62; 
-    ?channel_of_url: (Neturl.url -&#62; (in_channel * encoding option)) -&#62;
-    unit -&#62; 
-        resolver</PRE
->
-Reads from the local file system. Every file name is interpreted as
-file name of the local file system, and the referred file is read.</P
-><P
->The full form of a file URL is: file://host/path, where
-'host' specifies the host system where the file identified 'path'
-resides. host = "" or host = "localhost" are accepted; other values
-will raise Not_competent. The standard for file URLs is 
-defined in RFC 1738.</P
-><P
->Option <TT
-CLASS="LITERAL"
->~file_prefix</TT
->: Specifies how the "file:" prefix of
-file names is handled:
-            <P
-></P
-><UL
-COMPACT="COMPACT"
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Not_recognized:</TT
->The prefix is not
-recognized.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Allowed:</TT
-> The prefix is allowed but
-not required (the default).</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Required:</TT
-> The prefix is
-required.</P
-></LI
-></UL
-></P
-><P
->Option <TT
-CLASS="LITERAL"
->~host_prefix:</TT
-> Specifies how the "//host" phrase of
-file names is handled:
-            <P
-></P
-><UL
-COMPACT="COMPACT"
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Not_recognized:</TT
->The prefix is not
-recognized.</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Allowed:</TT
-> The prefix is allowed but
-not required (the default).</P
-></LI
-><LI
-STYLE="list-style-type: disc"
-><P
-><TT
-CLASS="LITERAL"
->`Required:</TT
-> The prefix is
-required.</P
-></LI
-></UL
-></P
-><P
->Option <TT
-CLASS="LITERAL"
->~system_encoding:</TT
-> Specifies the encoding of file
-names of the local file system. Default: UTF-8.</P
-><P
->Options <TT
-CLASS="LITERAL"
->~url_of_id</TT
->, <TT
-CLASS="LITERAL"
->~channel_of_url</TT
->: Not
-for the casual user!</P
-><P
-><PRE
-CLASS="PROGRAMLISTING"
->class combine : 
-    ?prefer:resolver -&#62; 
-    resolver list -&#62; 
-        resolver</PRE
->
-
-Combines several resolver objects. If a concrete entity with an
-<TT
-CLASS="LITERAL"
->ext_id</TT
-> is to be opened, the combined resolver tries the
-contained resolvers in turn until a resolver accepts opening the entity
-(i.e. it does not raise Not_competent on open_in).</P
-><P
->Clones: If the 'clone' method is invoked before 'open_in', all contained
-resolvers are cloned separately and again combined. If the 'clone' method is 
-invoked after 'open_in' (i.e. while the resolver is open), additionally the
-clone of the active resolver is flagged as being preferred, i.e. it is tried
-first. </P
-></DIV
-></DIV
-><DIV
-CLASS="NAVFOOTER"
-><HR
-ALIGN="LEFT"
-WIDTH="100%"><TABLE
-WIDTH="100%"
-BORDER="0"
-CELLPADDING="0"
-CELLSPACING="0"
-><TR
-><TD
-WIDTH="33%"
-ALIGN="left"
-VALIGN="top"
-><A
-HREF="c1567.html"
->Prev</A
-></TD
-><TD
-WIDTH="34%"
-ALIGN="center"
-VALIGN="top"
-><A
-HREF="index.html"
->Home</A
-></TD
-><TD
-WIDTH="33%"
-ALIGN="right"
-VALIGN="top"
-><A
-HREF="x1812.html"
->Next</A
-></TD
-></TR
-><TR
-><TD
-WIDTH="33%"
-ALIGN="left"
-VALIGN="top"
->Configuring and calling the parser</TD
-><TD
-WIDTH="34%"
-ALIGN="center"
-VALIGN="top"
-><A
-HREF="c1567.html"
->Up</A
-></TD
-><TD
-WIDTH="33%"
-ALIGN="right"
-VALIGN="top"
->The DTD classes</TD
-></TR
-></TABLE
-></DIV
-></BODY
-></HTML
->
\ No newline at end of file