There are a number of emacs commands for Specware usage. We also list some useful general-purpose commands. There is a Specware mode for editing Specware files.
These are the commands available when editing .sw files. Some of them are available in the Specware menu in the menubar.
| Key | Name | Description |
|---|---|---|
| tab | indent-line | Indents line based on context. |
| linefeed | newline-and-indent | Same as return followed by tab. |
| M-tab | back-to-outer-indent | Indents line for outer expression. |
| M-C-q | indent-sexp | Indents parenthesized expression following point. |
| M-C-\ | indent-region | Indents region. |
| M-* | switch-to-lisp | Switch to *Specware Shell* buffer. |
| M-. | meta-point | Prompts for op or type name (with default based on symbol at point), and goes to its definition. Searches only the units that have been loaded. First searches for definitions visible from the current unit. |
| M-, | continue-meta-point | If previous meta-point command returned more than one definition, go to the next definition. Can be repeated. |
| M-| | electric-pipe | Adds the skeleton of a new case to a case statement, properly indented. |
| C-c ; | comment-region | Comment out the region. With a negative argument uncomments the region. |
| C-c p | process-current-file | Does proc on current file. Also available in dired where it applies to the file on the current line. (This command will only work properly if the top-level directory for the file is in SWPATH). |
| C-c C-p | process-unit | Prompts for unitId to process. Defaults to unitId for the current file. |
| C-c g | generate-lisp | Does gen-lisp on current file. With an argument compiles and loads the generated lisp. |
| C-c C-l | generate-lisp | Does :swll on current file (generates lisp for local definitions of current file and compiles and loads them). |
| C-c ! | cd-current-directory | Does a :cd in the *Specware Shell* buffer to the directory of the current file. Also available in dired. |