The Twelf server is a stand-alone command interpreter which provides the
functionality of the
Twelf structure in ML (see section 9 ML Interface), but allows no ML definitions. It is significantly smaller
than Standard ML and is the recommended way to interact with Twelf
except for developers. Its behavior regarding configurations is
slightly different in that the server maintains a current configuration,
rather than allowing the binding of names to configurations.
Configuration are defined with the
Config.read command which
takes a configuration filename as argument.
In Emacs, the Twelf server typically runs in a process buffer
*twelf-server*. The user can select this buffer
and directly type commands to the Twelf server. This style
of interaction is inherited from the comint package for Emacs,
but typically one works through advanced commands in Twelf
mode (see section 11.1 Twelf Mode).
The Twelf server prompts with
%% OK %% or
%% ABORT %%
depending on the success of failure of the previous operation. It
accepts commands and their arguments on one line, except that additional
Twelf declarations which may be required are read separately, following
the command line. Reading declarations can be forcibly terminated
with the end-of-file token `%.'.
The server commands employ arguments of the following types.
RFS(see section 8.4 Search Strategies)
*(to indicate no limit) or a natural number
The Twelf server recognized the following commands.
set parameter value
Go to the first, previous, next, last section, table of contents.