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

12 Twelf Server

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

12.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
reconTraceMode
Either Progressive or Omniscient (see section 4.7 Tracing Reconstruction)
strategy
Either FRS or RFS (see section 10.4 Search Strategies)
tableStrategy
Either Variant or Subsumption (see section 5.9 Tabled Logic Programming)
bool
Either true or false
nat
A natural number (starting at 0)
limit
Either * (to indicate no limit) or a natural number

12.2 Server Commands

The Twelf server recognized the following commands.

set parameter value
Set parameter to value, where parameter is one of the following (explained in section 11.3 Environment Parameters).
chatter nat
doubleCheck bool
unsafe bool
Print.implicit bool
Print.depth limit
Print.length limit
Print.indent nat
Print.width nat
Trace.detail nat
Compile.optimize bool
Recon.trace bool
Recon.traceMode reconTraceMode
Prover.strategy strategy
Prover.maxSplit nat
Prover.maxRecurse nat
Table.strategy tableStrategy
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.subord
Print current subordination relation.
Print.domains
Print registered constraint domains.
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 timers.
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.
Config.append
Load current configuration without prior reset.
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).
Table.top
Enter interactive loop for tables queries (see section 5.9 Tabled Logic Programming).
help
Show available server commands, parameters, and server types.

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