14. Emacs Interface

The Twelf mode for Emacs provides some functions and utilities for editing Twelf source and for interacting with an inferior Twelf server process which can load configurations, files, and individual declarations and track the source location of errors. It also provides an interface to the tags package which allows simple editing of groups of files, constant name completion, and locating of constant declarations within the files of a configuration.

Note that in order to use the Emacs interface you need to include the line

(load "directory/emacs/twelf-init.el")

in your `.emacs' file, where directory is the Twelf root directory.

14.1 Twelf Mode

The Twelf mode in Emacs provides support for editing and indentation, syntax highlighting (including colors) (see section Syntax Highlighting), and communication commands for interacting with a Twelf server running as an inferior process to Emacs. It defines a menu which is added to the menu bar, usually at the top of each Emacs frame.

Many commands apply to the current declaration, which is the declaration in which we find the Emacs cursor (not the cursor of the window system). If the cursor is between declarations, the declaration after point is considered current. From the point of view of Emacs, single declarations never include consecutive blank lines, which provides some insulation against missing closing delimiters.

Normally, Twelf mode is entered automatically when a Twelf source file is edited (see section Emacs Initialization), but it can also be switched on or off directly with M-x twelf-mode.

M-x twelf-mode

Toggle Twelf mode, the major mode for editing Twelf code.

14.2 Editing Commands

The editing commands in Twelf mode partially analyse the structure of the text at the cursor position as Twelf code and try to indent accordingly. This is not always perfect.

TAB

M-x twelf-indent-line

Indent current line as Twelf code. This recognizes comments, matching delimiters, and standard infix operators.

DEL

M-x backward-delete-char-untabify

Delete character backward, changing tabs into spaces.

M-C-q

M-x twelf-indent-decl

Indent each line of the current declaration.

M-x twelf-indent-region

Indent each line of the region as Twelf code.

14.3 Type Checking Commands

The Twelf mode provides simple commands which cause the server to load or reload the current configuration, the file edited in the current buffer, or just the declaration at point. Each of these command can be preceded by a prefix argument (for example, C-u C-c C-c) which will select the Twelf server buffer after completion of the command. The Twelf server buffer can also be forced to be shown with the C-c C-u Emacs command.

C-c C-c

M-x twelf-save-check-config

Save its modified buffers and then check the current Twelf configuration. With prefix argument also displays Twelf server buffer. If necessary, this will start up an Twelf server process.

C-c C-a

M-x twelf-save-append-config

Save its modified buffers and then check the current Twelf configuration without resetting or reloading files unmodified since the last check. With prefix argument also displays Twelf server buffer. If necessary, this will start up an Twelf server process.

C-c C-s

M-x twelf-save-check-file

Save buffer and then check it by giving a command to the Twelf server. In Twelf Config minor mode, it reconfigures the server. With prefix argument also displays Twelf server buffer.

C-c C-d

M-x twelf-check-declaration

Send the current declaration to the Twelf server process for checking. With prefix argument also displays Twelf server buffer.

C-c c

M-x twelf-type-const

Display the type of the constant before point. Note that the type of the constant will be `absolute' rather than the type of the particular instance of the constant.

C-c C-u

M-x twelf-server-display

Display Twelf server buffer, moving to the end of output. With prefix argument also selects the Twelf server buffer.

14.4 Printing Commands

M-x twelf-print-signature

Prints the current signature in the Twelf server buffer.

M-x twelf-print-program

Prints the current signature as a program in the Twelf server buffer.

M-x twelf-print-subord

Prints the current subordination relation in the Twelf server buffer.

M-x twelf-print-tex-signature

Prints the current signature in TeX style. The output appears in the Twelf server buffer.

M-x twelf-print-tex-program

Prints the current signature as a program in TeX style. The output appears in the Twelf server buffer.

14.5 Tracing Commands

The Twelf Emacs mode provides a simple interface to the tracer. While tracing or breakpoints are on, you should be in the Emacs server buffer to type your input directly to the server as described in Tracing and Breakpoints.

M-x twelf-trace-trace

Read list of constants and trace them.

M-x twelf-trace-trace-all

Trace all clauses and families.

M-x twelf-trace-untrace

Untrace all clauses and families.

M-x twelf-trace-break

Read list of constants and set breakpoints.

M-x twelf-trace-break-all

Set breakpoints on all clauses and families.

M-x twelf-trace-unbreak

Remove all breakpoints.

M-x twelf-trace-show

Show tracing and breakpoint information.

14.6 Error Tracking

Error messages by the Twelf server are flagged with the filename and an educated guess as to the source of the error (see section Error Messages). These can be interpreted by Emacs to jump directly to the suspected site.

Sometimes, the server buffer and the the server itself believe to have different working directories. In that case, error tracking may not be able to find the file, and an explicit call to OS.chDir or M-x cd in the server buffer may be required.

C-c `

M-x twelf-next-error

Find the next error by parsing the Twelf server or Twelf-SML buffer. Move the error message on the top line of the window; put the cursor at the beginning of the error source. If the error message specifies a range, the mark is placed at the end.

C-c =

M-x twelf-goto-error

Go to the error reported on the current line or below. Also updates the error cursor to the current line.

14.7 Server State

The server state consists of the current configuration and a number of parameters described in Twelf Server. The current configuration is often set implicitly, with the C-c C-c command in a configuration buffer, but it can also be set explicitly.

C-c <

M-x twelf-set

Sets the Twelf parameter PARM to VALUE. When called interactively, prompts for parameter and value, supporting completion.

C-c >

M-x twelf-get

Prints the value of the Twelf parameter PARM. When called interactively, prompts for parameter, supporting completion.

C-c C-i

M-x twelf-server-interrupt

Interrupt the Twelf server process.

M-x twelf-server

Start an Twelf server process in a buffer named *twelf-server*. Any previously existing process is deleted after confirmation. Optional argument PROGRAM defaults to the value of the variable twelf-server-program. This locally re-binds `twelf-server-timeout' to 15 secs.

M-x twelf-server-configure

Initializes the Twelf server configuration from CONFIG-FILE. A configuration file is a list of relative file names in dependency order. Lines starting with % are treated as comments. Starts a Twelf servers if necessary.

M-x twelf-reset

Reset the global signature of Twelf maintained by the server.

M-x twelf-server-quit

Kill the Twelf server process.

M-x twelf-server-restart

Restarts server and re-initializes configuration. This is primarily useful during debugging of the Twelf server code or if the Twelf server is hopelessly wedged.

M-x twelf-server-send-command

Restarts server and re-initializes configuration. This is primarily useful during debugging of the Twelf server code or if the Twelf server is hopelessly wedged.

14.8 Info File

The content of this file in Info format can be visited directly and does not need to be tied into the Info tree. See the documentation for the Emacs info package for more info

C-c C-h

M-x twelf-info

Visit the Twelf User's Guide in info format in Emacs. With a prefix argument it prompts for the info file name, which defaults to the value of the twelf-info-file variable.

14.9 Tags Files

Tags files provide a convenient way to group files, such as Twelf configurations. See the documentation for the Emacs etags package for more information.

M-x twelf-tag

Create tags file for current configuration. If the current configuration is sources.cfg, the tags file is TAGS. If current configuration is named FILE.cfg, tags file will be named FILE.tag Errors are displayed in the Twelf server buffer.

M-.

M-x find-tag TAG

Selects the buffer that the tag is contained in and puts point at its definition.

C-x 4 .

M-x find-tag-other-window TAG

Selects the buffer that TAG is contained in in another window and puts point at its definition.

C-c q

M-x tags-query-replace FROM TO

Query-replace-regexp FROM with TO through all files listed in tags table.

C-c s

M-x tags-search REGEXP

Search through all files listed in tags table for match for REGEXP.

M-,

M-x tags-loop-continue

Continue last C-c s or C-c q command.

14.10 Twelf Timers

The following commands obtain the runtime statistics of the the Twelf server.

M-x twelf-timers-reset

Reset the Twelf timers.

M-x twelf-timers-show

Show and reset the Twelf timers.

M-x twelf-timers-check

Show the Twelf timers without resetting them.

14.11 Twelf-SML Mode

There is some support for interacting with Twelf, even when it is run within ML, rather than as a stand-alone server. You can start an SML in which you intend to run Twelf with M-x twelf-sml; the buffer will then be in Twelf-SML mode.

If you intend to send command to a buffer running Twelf in SML (rather than the Twelf server), you can switch to a minor mode 2Twelf-SML with M-x twelf-to-twelf-sml.

M-x twelf-sml

Run an inferior Twelf-SML process in a buffer *twelf-sml*. If there is a process already running in *twelf-sml*, just switch to that buffer. With argument, allows you to change the program which defaults to the value of twelf-sml-program. Runs the hooks from twelf-sml-mode-hook (after the comint-mode-hook is run).

M-x twelf-to-twelf-sml-mode

Toggles minor mode for sending queries to Twelf-SML instead of Twelf server.

C-c C-e

M-x twelf-sml-send-query

Send the current declaration to the inferior Twelf-SML process as a query. Prefix argument means switch-to-twelf-sml afterwards.

C-c C-r

M-x twelf-sml-send-region

Send the current region to the inferior Twelf-SML process. Prefix argument means switch-to-twelf-sml afterwards.

C-c RETURN

M-x twelf-sml-send-newline

Send a newline to the inferior Twelf-SML process. If a prefix argument is given, switches to Twelf-SML buffer afterwards.

C-c ;

M-x twelf-sml-send-semicolon

Send a semi-colon to the inferior Twelf-SML process. If a prefix argument is given, switched to Twelf-SML buffer afterwards.

C-c d

M-x twelf-sml-cd DIR

Make DIR become the Twelf-SML process' buffer's default directory and furthermore issue an appropriate command to the inferior Twelf-SML process.

M-x twelf-sml-quit

Kill the Twelf-SML process.

14.12 Emacs Variables

A number of Emacs variables can be changed to customize the behavior of Twelf mode. The list below is not complete; please refer to the Emacs Lisp sources in emacs/twelf.el for additional information.

twelf-indent

Indent for Twelf expressions.

twelf-server-program

Default Twelf server program.

twelf-info-file

Default Twelf info file.

twelf-mode-hook

List of hook functions to run when switching to Twelf mode.

twelf-server-mode-hook

List of hook functions to run when switching to Twelf Server mode.

twelf-sml-program

Default Twelf-SML program.

twelf-sml-mode-hook

List of hook functions for Twelf-SML mode.

14.13 Syntax Highlighting

Twelf also provides syntax highlighting, which helps make Elf code more readable. This highlighting can use different colors and faces. Unfortunately, the necessary libraries are at present not standardized between XEmacs and FSF Emacs, which means that highlighting support is less general and less portable than the plain Twelf mode.

At present, highlighting has not been extensively tested in various versions of Emacs, but the font-lock mode provided in `emacs/twelf-font.el' seems to work at least in XEmacs version 19.16 and FSF Emacs version 19.34. The alternative highlight mode provided in `emacs/twelf-hilit' appears to work in FSF Emacs 19.34.

Unlike other font-lock modes, Twelf's fontification is not `electric' in that it does not fontify as one types. One has to explicitly issue a command to fontify the current Twelf declaration or current buffer, since single-line highlighting is too error-prone and multi-line immediate highlighting is not well supported in current versions of font lock mode.

C-c C-l

M-x twelf-font-fontify-decl

Fontifies the current Twelf declaration.

C-c l

M-x twelf-font-fontify-buffer

Fontitifies the current buffer as Twelf code

M-x twelf-font-unfontify

Removes fontification from current buffer.

14.14 Emacs Initialization

If Twelf has been properly installed, you can use the Twelf's Emacs interface with the default settings simply by adding the line

(load "directory/emacs/twelf-init.el")

to your `.emacs' file, where directory is the Twelf root directory. In order to customize the behavior, you might copy the file `emacs/twelf-init.el' or its contents and change it as appropriate.

14.15 Command Summary

--- Editing Commands ---
TAB          twelf-indent-line
DEL          backward-delete-char-untabify
M-C-q        twelf-indent-decl

--- Type Checking ---
C-c C-c      twelf-save-check-config
C-c C-a      twelf-save-append-config
C-c C-s      twelf-save-check-file
C-c C-d      twelf-check-declaration
C-c c        twelf-type-const
C-c C-u      twelf-server-display

--- Error Tracking ---
C-c `        twelf-next-error
C-c =        twelf-goto-error

--- Syntax Highlighting ---
C-c C-l      twelf-font-fontify-decl
C-c l        twelf-font-fontify-buffer

--- Server State ---
C-c <        twelf-set
C-c >        twelf-get
C-c C-i      twelf-server-interrupt
M-x twelf-server
M-x twelf-server-configure
M-x twelf-server-quit
M-x twelf-server-restart
M-x twelf-server-send-command

--- Info ---
C-c C-h      twelf-info

--- Timers ---
M-x twelf-timers-reset
M-x twelf-timers-show
M-x twelf-timers-check

--- Tags (standard Emacs etags package) ---
M-x twelf-tag
M-.          find-tag (standard binding)
C-x 4 .      find-tag-other-window (standard binding)
C-c q        tags-query-replace (Twelf mode binding)
C-c s        tags-search (Twelf mode binding)
M-,          tags-loop-continue (standard binding)
             visit-tags-table, list-tags, tags-apropos

--- Communication with inferior Twelf-SML process (not Twelf Server) ---
M-x twelf-sml
C-c C-e      twelf-sml-send-query
C-c C-r      twelf-sml-send-region
C-c RET      twelf-sml-send-newline
C-c ;        twelf-sml-send-semicolon
C-c d        twelf-sml-cd
M-x twelf-sml-quit

--- Variables ---
twelf-indent

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