13. Twelf Server

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

13.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 Tracing Reconstruction)

strategy

Either FRS or RFS (see section Search Strategies)

tableStrategy

Either Variant or Subsumption (see section 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

13.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 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 Interactive Queries).

Table.top

Enter interactive loop for tables queries (see section Tabled Logic Programming).

version

Show server version.

help

Show available server commands, parameters, and server types.

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.