]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/pxp/pxp/doc/manual/html/x1965.html
Initial revision
[helm.git] / helm / DEVEL / pxp / pxp / doc / manual / html / x1965.html
diff --git a/helm/DEVEL/pxp/pxp/doc/manual/html/x1965.html b/helm/DEVEL/pxp/pxp/doc/manual/html/x1965.html
new file mode 100644 (file)
index 0000000..8fc8562
--- /dev/null
@@ -0,0 +1,152 @@
+<HTML
+><HEAD
+><TITLE
+>Updates</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="Invoking the parser"
+HREF="x1818.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="x1818.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"
+>&nbsp;</TD
+></TR
+></TABLE
+><HR
+ALIGN="LEFT"
+WIDTH="100%"></DIV
+><DIV
+CLASS="SECT1"
+><H1
+CLASS="SECT1"
+><A
+NAME="AEN1965"
+>4.5. Updates</A
+></H1
+><P
+><I
+CLASS="EMPHASIS"
+>Some (often later added) features that are otherwise
+not explained in the manual but worth to be mentioned.</I
+></P
+><P
+></P
+><UL
+COMPACT="COMPACT"
+><LI
+STYLE="list-style-type: disc"
+><P
+>Methods node_position, node_path, nth_node,
+previous_node, next_node for nodes: See pxp_document.mli</P
+></LI
+><LI
+STYLE="list-style-type: disc"
+><P
+>Functions to determine the document order of nodes:
+compare, create_ord_index, ord_number, ord_compare: See pxp_document.mli</P
+></LI
+></UL
+></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="x1818.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"
+>&nbsp;</TD
+></TR
+><TR
+><TD
+WIDTH="33%"
+ALIGN="left"
+VALIGN="top"
+>Invoking the parser</TD
+><TD
+WIDTH="34%"
+ALIGN="center"
+VALIGN="top"
+><A
+HREF="c1567.html"
+>Up</A
+></TD
+><TD
+WIDTH="33%"
+ALIGN="right"
+VALIGN="top"
+>&nbsp;</TD
+></TR
+></TABLE
+></DIV
+></BODY
+></HTML
+>
\ No newline at end of file