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

11 Twelf Server

The Twelf server is a stand-alone command interpreter which provides the functionality of the Twelf structure in ML (see section 10 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 12.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 `%.'.

11.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 9.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

11.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 10.3 Environment Parameters).
chatter nat
doubleCheck bool
Twelf.unsafe bool
Print.implicit bool
Print.depth limit
Print.length limit
Print.indent nat
Print.width nat
Trace.detail nat
Prover.strategy strategy
Prover.maxSplit nat
Prover.maxRecurse nat
get parameter
Print the current value of parameter (see table above).
Trace.trace id1 ... idn
Trace given constants
Trace.traceAll
Trace all constants
Trace.untrace
Untrace all constants
Trace.break id1 ... idn
Set breakpoint for given constants
Trace.breakAll
Break on all constants
Trace.unbreak
Remove all breakpoints
Trace.show
Show current trace and breakpoints
Trace.reset
Reset all tracing and breaking
Print.sgn
Print current signature
Print.prog
Print current signature as program
Print.TeX.sgn
Print current signature in TeX format
Print.TeX.prog
Print current signature in TeX format as program
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
make file
Read and load current configuration from file.
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.