1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
;;; Commentary:
;; emacs-acl2.el
;;; Here we summarize the functionality offered by this file. In many cases,
;;; lower-level details may be found later in the file where the functionality
;;; is actually provided.
; General shell stuff
; Starts up a shell buffer, *shell*.
; "meta-x new-shell" starts new shell buffers *shell-1*, *shell-2*, ....
; "control-x k" redefined to avoid accidentally killing shell buffer.
; "control-t e" sends the current form to the shell buffer.
; "control-t b" switches to the shell buffer.
; "control-t c" sets the shell buffer (initially, *shell*) to the current
; buffer
; "control-t control-e" sends the current form to the shell buffer,
; but in a different window. If the shell buffer is already
; visible in some window, use that window. Otherwise, use the
; "other window" as defined by Emacs (see the Emacs
; documentation for `other-window').
; "control-d" is redefined in shell/telnet buffers to avoid ending process.
; "meta-p" and "meta-n" cycle backward/forward doing command completion in
; shell/telnet buffers.
; "control-<RETURN>" sets shell/telnet directory buffer to current directory.
; From current buffer to shell buffer
; "control-t l" prints appropiate ACL2 LD form to the end of the shell
; buffer, to cause evaluation of the active region in the current
; buffer.
; "control-t control-l" prints just as above, but inhibits output and proofs;
; can easily be edited to inhibit only one or the other
; "control-t u" puts an appropriate :ubt at the end of the shell buffer, based
; on the event in which you are currently standing.
; Some editing commands
; "meta-x find-unbalanced-parentheses" locates unbalanced parentheses.
; "control-t a" puts line with cursor at bottom of window.
; "control-t <TAB>" completes filename in any buffer.
; "control-t control-v" scrolls half as far as "control-v".
; "control-t v" scrolls half as far as "meta-v".
; "control-t s" searches forward non-interactively, with string supplied in
; minibuffer, case-sensitive
; "control-t control-s": like "control-t s" above, but case-insensitive (at
; least by default).
; "control-meta-q" indents s-expression even when not in lisp-mode.
; "control-t control-p" executes "meta-x up-list", moving to end of enclosing
; s-expression.
; "control-t p" compares the current form with one obtained with
; meta-. (see below for more details).
; "control-t w" does "meta-x compare-windows" (see emacs documentation,
; "control-h f compare-windows", for more info).
; "control-t q" is like "control-t w" above, but ignores whitespace (and case
; too, with a positive prefix argument).
; Lisp mode comes up with auto-fill mode on, right margin set at column 79,
; tabs interpreted using spaces, and a single ";" comment staying on the
; left margin (search for lisp-mode-hook below).
; If X Windows is being run, then font-lock-mode is also turned on,
; which causes Emacs to color text in .lisp files. If you don't want
; colors in .lisp files, put this in your .emacs file after the load of
; "emacs-acl2.el":
; (if (equal window-system 'x)
; (remove-hook 'lisp-mode-hook '(lambda () (font-lock-mode 1))))
; "meta-x visit-acl2-tags-table" sets the current tag table to the one in the
; ACL2 source directory.
; "meta-," is defined to be tags-loop-continue, which is how it has
; traditionally been defined by Emacs but might be defined
; differently in some versions of Emacs 25 (and perhaps later).
; NOTE:
; Put (setq *preserve-tags-loop-continue* t) in your .emacs
; file before loading the present file, if you want to avoid
; redefining "meta-,".
; "control-t f" fills format strings; see documentation for more info
; ("control-h f fill-format-string").
; "control-t control-f" buries the current buffer (puts it on the bottom of
; the buffer stack, out of the way, without killing the buffer)
; ACL2 proof-tree support
; NOTE: This works by default if you install the ACL2 community books, as
; most ACL2 users do, in the books/ directory of your ACL2
; distribution. Otherwise, you will need to set the variable
; *acl2-interface-dir* to a directory string containing a file
; top-start-shell-acl2.el that defines the functions start-proof-tree
; and start-proof-tree-noninteractive in emacs. For user-level
; documentation provided in the ACL2 community books implementation,
; see the following file included there:
; books/interface/emacs/PROOF-TREE-EMACS.txt
; "meta-x start-proof-tree" starts proof-tree tracking in the current buffer
; (where ACL2 is running). See ACL2 documentation for PROOF-TREE for
; more information.
; Function start-proof-tree-noninteractive (see below) can be used to start
; proof-trees when emacs starts up; see below.
; Run ACL2 as inferior process
; NOTE: This works by default if you install the ACL2 community books.
; Otherwise, see the NOTE above on "ACL2 proof-tree support".
; "meta-x run-acl2" starts up acl2 as an inferior process in emacs. You may
; have better luck simply issuing your ACL2 command in an ordinary
; (emacs) shell.
; ACL2 proof-builder support
; "control-t d" prints an appropriate DV command at the end of the current
; buffer, suitable for diving to subexpression after printing with
; proof-builder "th" or "p" command and then positioning cursor on that
; subexpression. See ACL2 documentation for PROOF-BUILDER.
; "control-t control-d" is like "control-t d" above, but for DIVE instead
; (used with "pp" instead of "p")
; Load other tools
; Support for Dynamic Monitoring of Rewrites (dmr)
; "control-t 1" to start dmr, "control-t 2" to stop dmr
; Support for ACL2-Doc browser
; "control-t g" to start the ACL2-Doc browser
; Support for xdoc-link-mode, used by acl2+books XDOC manual
; Miscellaneous
; "meta-x acl2-info" brings up ACL2 documentation in pleasant emacs-info
; format.
; "meta-x date" prints the current date and time (commented out).
; "control-meta-l" swaps top buffer with next-to-top buffer (same as
; "control-x b <RETURN>").
; "control-t" is a prefix for other commands
; "control-t control-t" transposes characters (formerly "control-t")
; Other features:
; Turn on time/mail display on mode line.
; Disable a few commands.
; Calls of case, case!, case-match, and dolist will indent like
; calls of defun.
; Some other features you may want (these are commented out by default):
; Turn off menu bar.
; Turn off emacs auto-save feature.
; Start an abbrev table.
; Avoid getting two windows, for example with control-x control-b.
; Modify whitespace to ignore with "control-t q" (see above).
; Turn on version control.
; Arrange for "control-meta-l" to work as above even in rmail mode.
; If time and "mail" displays icons, this may turn them into ascii.
; Get TeX-style quotes with meta-".
; Debug emacs errors with backtrace and recursive edit.
;; acl2-mode.el
;; The base major mode for editing Acl2 code.
;; This mode extends very slightly lisp-mode.el (documented in the Emacs manual).
;; See also inf-acl2.el inf-acl2-mouse.el and inf-acl2-menu.el
;; inf-acl2.el
;;; Hacked from inf-lisp.el, Feb 17 94 MKS
;;; Hacked from tea.el by Olin Shivers (shivers@cs.cmu.edu). 8/88
;;; This file defines an acl2-in-a-buffer package (inferior-acl2
;;; mode) built on top of comint mode. This version is more
;;; featureful, robust, and uniform than the Emacs 18 version. The
;;; key bindings are also more compatible with the bindings of Hemlock
;;; and Zwei (the Lisp Machine emacs).
;;; Since this mode is built on top of the general command-interpreter-in-
;;; a-buffer mode (comint mode), it shares a common base functionality,
;;; and a common set of bindings, with all modes derived from comint mode.
;;; This makes these modes easier to use.
;;; For documentation on the functionality provided by comint mode, and
;;; the hooks available for customising it, see the file comint.el.
;;; For further information on inferior-lisp mode, see the comments below.
;;; Needs fixin:
;;; The load-file/compile-file default mechanism could be smarter -- it
;;; doesn't know about the relationship between filename extensions and
;;; whether the file is source or executable. If you compile foo.lisp
;;; with compile-file, then the next load-file should use foo.bin for
;;; the default, not foo.lisp. This is tricky to do right, particularly
;;; because the extension for executable files varies so much (.o, .bin,
;;; .lbin, .mo, .vo, .ao, ...).
;;;
;;; It would be nice if inferior-lisp (and inferior scheme, T, ...) modes
;;; had a verbose minor mode wherein sending or compiling defuns, etc.
;;; would be reflected in the transcript with suitable comments, e.g.
;;; ";;; redefining fact". Several ways to do this. Which is right?
;;;
;;; When sending text from a source file to a subprocess, the process-mark can
;;; move off the window, so you can lose sight of the process interactions.
;;; Maybe I should ensure the process mark is in the window when I send
;;; text to the process? Switch selectable?
|
