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


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

11.1 Twelf Mode

The Twelf mode in Emacs provides support for editing and indentation, syntax highlighting (including colors) (see section 11.11 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 11.12 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.

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

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

11.4 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 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.

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.

11.5 Server State

The server state consists of the current configuration and a number of parameters described in section 10 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, promts 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.

11.6 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.

11.7 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.

11.8 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.

11.9 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.

11.10 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.

11.11 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.

11.12 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.

11.13 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-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.