← Back to branch summary

~ubuntu-branches/ubuntu/trusty/pxp/trusty

« back to all changes in this revision

Viewing changes to doc/manual/html/ref/Pxp_document.extension-c.html

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2013-07-11 11:21:26 UTC
  • mfrom: (6.1.3 sid)
  • Revision ID: package-import@ubuntu.com-20130711112126-5wysiuf0cgjo376r
Tags: 1.2.4-1
* Team upload
* New upstream release
* Update Vcs-*

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/manual/html/ref/Pxp_document.extension-c.html
37
37
<link title="Example_readme" rel="Chapter" href="Example_readme.html"><title>PXP Reference : Pxp_document.extension</title>
38
38
</head>
39
39
<body>
40
 
<div class="navbar">&nbsp;<a href="Pxp_document.html">Up</a>
41
 
&nbsp;<a href="Pxp_document.node-c.html">Next</a>
 
40
<div class="navbar">&nbsp;<a class="up" href="Pxp_document.html" title="Pxp_document">Up</a>
 
41
&nbsp;<a class="post" href="Pxp_document.node-c.html" title="Pxp_document.node">Next</a>
42
42
</div>
43
 
<center><h1>Class type <a href="type_Pxp_document.extension.html">Pxp_document.extension</a></h1></center>
44
 
<br>
45
 
<pre><span id="TYPEextension"><span class="keyword">class type</span> <code class="type">['a]</code> extension</span> = <code class="code"><span class="keyword">object</span></code> <a href="Pxp_document.extension-c.html">..</a> <code class="code"><span class="keyword">end</span></code></pre>The <code class="code">extension</code> is, as the name says, the extensible part of the
 
43
<h1>Class type <a href="type_Pxp_document.extension.html">Pxp_document.extension</a></h1>
 
44
<pre><span id="TYPEextension"><span class="keyword">class type</span> <code class="type">['node]</code> extension</span> = <code class="code"><span class="keyword">object</span></code> <a href="Pxp_document.extension-c.html">..</a> <code class="code"><span class="keyword">end</span></code></pre>The <code class="code">extension</code> is, as the name says, the extensible part of the
46
45
    nodes. See <a href="Intro_extensions.html"><code class="code"><span class="constructor">Intro_extensions</span></code></a> for an introduction into extensions.<br>
47
46
<hr width="100%">
48
 
<pre><span id="METHODclone"><span class="keyword">method</span> clone</span> : <code class="type">< clone : 'b; node : 'a; set_node : 'a -> unit; .. > as 'b</code></pre><div class="info">
 
47
<pre><span id="METHODclone"><span class="keyword">method</span> clone</span> : <code class="type">< clone : 'a; node : 'node; set_node : 'node -> unit; .. > as 'a</code></pre><div class="info">
49
48
<code class="code">clone</code> is called when the node is to be duplicated, and as a
50
49
          followup action, also the extension must be cloned. This method
51
50
          must return a deep copy of the extension. By convention, the
52
51
          caller of this method must also invoke <code class="code">set_node</code> on the copied
53
52
          extension to establish a new link to a main node.<br>
54
53
</div>
55
 
<pre><span id="METHODnode"><span class="keyword">method</span> node</span> : <code class="type">'a</code></pre><div class="info">
 
54
<pre><span id="METHODnode"><span class="keyword">method</span> node</span> : <code class="type">'node</code></pre><div class="info">
56
55
<code class="code">node</code> is the link from the extension to the main node.
57
56
          Conventionally, this link is set by the node via <code class="code">set_node</code>
58
57
          below after the extension has been created or cloned.<br>
59
58
</div>
60
 
<pre><span id="METHODset_node"><span class="keyword">method</span> set_node</span> : <code class="type">'a -> unit</code></pre><div class="info">
 
59
<pre><span id="METHODset_node"><span class="keyword">method</span> set_node</span> : <code class="type">'node -> unit</code></pre><div class="info">
61
60
<code class="code">set_node n</code> sets the link to the main node to <code class="code">n</code>. The link is
62
61
          returned by <code class="code">node</code> after that.<br>
63
62
</div>