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.
The Twelf mode in Emacs provides support for editing and indentation, syntax highlighting (including colors) (see section 13.13 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 13.14 Emacs Initialization), but it can also be switched on or off directly with M-x twelf-mode.
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.
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.
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 section 11.5 Tracing and Breakpoints.
Error messages by the Twelf server are flagged with the filename and an educated guess as to the source of the error (see section 4.6 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.
The server state consists of the current configuration and a number of parameters described in section 12 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.
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
twelf-info-file variable.
Tags files provide a convenient way to group files, such as Twelf configurations. See the documentation for the Emacs etags package for more information.
The following commands obtain the runtime statistics of the the Twelf server.
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.
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
twelf-server-program
twelf-info-file
twelf-mode-hook
twelf-server-mode-hook
twelf-sml-program
twelf-sml-mode-hook
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.
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.
--- 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-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
Go to the first, previous, next, last section, table of contents.