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
|
;; Add key interface for prooftree buffers.
;; March 3 95 MKS
;; ----------------------------------------------------------------------
;; USER SETTINGS
;; (defvar *acl2-proof-tree-height* 17)
;; (defvar *checkpoint-recenter-line* 3)
;; ----------------------------------------------------------------------
;; Load all of the various acl2-interface files, if necessary.
(load "mfm-acl2.el") ;(require 'mfm-acl2)
;; (load "interface-macros.el") ;(require 'interface-macros)
;; Replaced by the following defvar and four functions, which is all this
;; file used from interface macros.
;; Begin insert
(defvar mode-menu-alist nil)
;; WARNING: Be sure that if should-i-install, update-mode-menu-alist,
;; remove-mode-menu-alist, define-mode-keys, or extend-hook is changed, then it
;; is also changed in key-interface.el.
(defun should-i-install (mode feature)
;; mode is mode-name
(memq feature (cdr (assoc mode mode-menu-alist))))
(defun update-mode-menu-alist (l)
(if (not (consp (car l)))
(setq l (cons l nil)))
(setq mode-menu-alist
(append l (remove-mode-menu-alist mode-menu-alist l))))
(defun remove-mode-menu-alist (alist l)
(cond ((null alist) l)
((assoc (car (car alist)) l)
(remove-mode-menu-alist (cdr alist) l))
(t (cons (car alist) (remove-mode-menu-alist (cdr alist) l)))))
(defun define-mode-keys (mode-map-name mode-map keys)
;; An entry in keys may have two forms:
;; (key function)
;; (keymap key function)
;; The second allows you to create subkeymaps, e.g. Control-Z
(if (should-i-install mode-map-name 'keys)
(mapcar
(function (lambda (x)
(if (equal (length x) 2)
(define-key mode-map (car x) (car (cdr x)))
(if (keymapp (eval (car x)))
(define-key (eval (car x)) (car (cdr x)) (car (cdr (cdr x))))
(error
(format "Keymap %s not defined in mode %s" (car x) (car mode-map)))))))
keys)))
(defun extend-hook (hook entry)
;; Add an entry onto a mode-hook, being sensitive to the
;; stupid Emacs permission for it to be a function or list
;; of functions.
(cond ((null hook) (list entry))
((symbolp hook) (if (not (equal entry hook)) (list hook entry) hook))
((not (consp hook))
(message (format "Strange hook, %s, replaced by %s." hook entry))
(list entry))
((equal (car hook) 'lambda)
(list hook entry))
((member-equal entry hook) hook)
(t (append hook (list entry)))))
;; end insert
(update-mode-menu-alist *acl2-user-map-interface*)
;; Defined in mfm-acl2 so that checkpoint-help can use it.
(defvar prooftree-subkey)
(setq prooftree-subkey "\C-z")
;; prooftree-subkeymap was set by prooftree-mode.el. Now do it here.
(defvar prooftree-subkeymap (make-sparse-keymap))
(defvar old-prooftree-subkey (global-key-binding prooftree-subkey))
(define-key (current-global-map) prooftree-subkey prooftree-subkeymap)
(defconst prooftree-keys
; WARNING: Keep this in sync with the corresponding definition in
; acl2-interface.el.
(list
(list 'prooftree-subkeymap "z" old-prooftree-subkey)
(list 'prooftree-subkeymap "c" 'checkpoint)
(list 'prooftree-subkeymap "s" 'suspend-proof-tree)
(list 'prooftree-subkeymap "r" 'resume-proof-tree)
(list 'prooftree-subkeymap "g" 'goto-subgoal)
(list 'prooftree-subkeymap "h" 'checkpoint-help)
(list 'prooftree-subkeymap "?" 'checkpoint-help)
(list 'prooftree-subkeymap "o" 'select-other-frame-with-focus)
(list 'prooftree-subkeymap "b" 'visit-proof-tree)
(list 'prooftree-subkeymap "B" 'visit-proof-tree-other-frame)))
(define-mode-keys 'global (current-global-map) prooftree-keys)
(provide 'key-interface)
|
