Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
d95c289b
Commit
d95c289b
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-07-02 18:10:14 by cvscast] Forgot a few points in the manual -- Alain
Original author: cvscast Date: 2003-07-02 18:10:14+00:00
parent
604979bd
Changes
1
Hide whitespace changes
Inline
Side-by-side
web/manual/interpreter.xml
View file @
d95c289b
...
...
@@ -130,6 +130,11 @@ Filename are relative to the directory of the current file
(or the current directory in the toplevel).
</li>
<li>
Global namespace binding
<code>
namespace %%p%% = "%%...%%"
</code>
and global namespace default
<code>
namespace "%%...%%"
</code>
(see
<local
href=
"namespaces"
/>
).
</li>
</ul>
</box>
...
...
@@ -152,8 +157,8 @@ must be contained in a single adjacent sequence of phrases
You can quit the toplevel with the toplevel directive
<code>
#quit
</code>
but also with either
<code>
Ctrl-C
</code>
or
<code>
Ctrl-D
</code>
. In order to allow persistence
(option
<code>
-
-dump
</code>
) to operate,
you must quit the toplevel with
<code>
#quit
</code>
.
(option
s
<code>
-
save
</code>
,
<code>
--load
</code>
and
<code>
--dump
</code>
) to operate,
you must quit the toplevel with
<code>
#quit
</code>
.
</p>
<p>
...
...
@@ -164,6 +169,12 @@ for parsing (as defined by the user) and
for pretty-printing (as computed by CDuce itself).
</p>
<p>
The toplevel directive
<code>
#reinit_ns
</code>
reinit the
table of prefix-to-namespace bindings used for pretty-printing
values and types with namespaces (see
<local
href=
"namespaces"
/>
).
</p>
<p>
The toplevel has no line editing facilities.
You can use an external wrapper such as
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment