Go to the first, previous, next, last section, table of contents.

10 Twelf Server

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 called *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 `%.'.

10.1 Server Types

The server commands employ arguments of the following types.

file
The name of a file, relative to the current working directory.
id
A Twelf identifier
strategy
Either FRS or RFS (see section 8.4 Search Strategies)
bool
Either true or false
nat
A natural number (starting at 0)
limit
Either * (to indicate no limit) or a natural number

10.2 Server Commands

The Twelf server recognized the following commands.

set parameter value
Set parameter to value, where parameter is on of the following (explained in section 9.3 Environment Parameters).
chatter nat
doubleCheck bool
Print.implicit bool
Print.depth limit
Print.length limit
Print.indent nat
Print.width nat
Prover.strategy strategy
Prover.maxSplit nat
Prover.maxRecurse nat
get parameter
Print the current value of parameter (see table above).
Timers.show
Print and reset timers.
Timers.reset
Reset timers.
Timers.check
Print, but do not reset timrs.
OS.chDir file
Change working directory to file.
OS.getDir
Print current working directory.
OS.exit
Exit Twelf server.
quit
Quit Twelf server (same as exit).
Config.read file
Read current configuration from file.
Config.load
Load current configuration
reset
Reset global signature.
loadFile file
Load Twelf file file.
decl id
Show constant declaration for id.
top
Enter interactive query loop (see section 5.3 Interactive Queries)

Go to the first, previous, next, last section, table of contents.