2938
|
1 |
;
|
|
2 |
; $Id$
|
|
3 |
;
|
3304
|
4 |
; Setup Emacs for Isabelle environment.
|
2938
|
5 |
;
|
|
6 |
|
3304
|
7 |
;; Misc settings
|
2972
|
8 |
|
3304
|
9 |
(setq isa-use-sml-mode nil)
|
2972
|
10 |
|
|
11 |
|
3304
|
12 |
;; Fonts and Keymaps
|
2938
|
13 |
|
|
14 |
(setq default-ctl-arrow "z")
|
|
15 |
(setq ctl-arrow "z")
|
|
16 |
|
3304
|
17 |
(if (eq isa-emacs-version 'isa-19)
|
|
18 |
(progn
|
|
19 |
(standard-display-8bit 128 255)
|
|
20 |
;; FIXME
|
|
21 |
;; DO NOT EDIT the lines between BEGIN-KEY-MAP and END-KEY-MAP
|
|
22 |
;; the table is generated by the perl script `gen-isa_gnu_emacs'
|
|
23 |
;; In order to make changes to the keyboard mappings you should edit
|
|
24 |
;; the configuration file `key-table.inp' which is interpreted by
|
|
25 |
;; the perl script `gen-isa_gnu_emacs',
|
|
26 |
;;
|
|
27 |
;;
|
|
28 |
;; key-map for Isabelle font
|
|
29 |
;;
|
|
30 |
;; BEGIN-KEY-MAP
|
|
31 |
(global-set-key [?\s-G] '(lambda () (interactive) (insert "\241")))
|
|
32 |
(global-set-key [?\s-D] '(lambda () (interactive) (insert "\242")))
|
|
33 |
(global-set-key [?\s-J] '(lambda () (interactive) (insert "\243")))
|
|
34 |
(global-set-key [?\s-L] '(lambda () (interactive) (insert "\244")))
|
|
35 |
(global-set-key [?\s-P] '(lambda () (interactive) (insert "\245")))
|
|
36 |
(global-set-key [?\s-S] '(lambda () (interactive) (insert "\246")))
|
|
37 |
(global-set-key [?\s-F] '(lambda () (interactive) (insert "\247")))
|
|
38 |
(global-set-key [?\s-Q] '(lambda () (interactive) (insert "\250")))
|
|
39 |
(global-set-key [?\s-W] '(lambda () (interactive) (insert "\251")))
|
|
40 |
(global-set-key [?\s-a] '(lambda () (interactive) (insert "\252")))
|
|
41 |
(global-set-key [?\s-b] '(lambda () (interactive) (insert "\253")))
|
|
42 |
(global-set-key [?\s-g] '(lambda () (interactive) (insert "\254")))
|
|
43 |
(global-set-key [?\s-d] '(lambda () (interactive) (insert "\255")))
|
|
44 |
(global-set-key [?\s-e] '(lambda () (interactive) (insert "\256")))
|
|
45 |
(global-set-key [?\s-z] '(lambda () (interactive) (insert "\257")))
|
|
46 |
(global-set-key [?\s-h] '(lambda () (interactive) (insert "\260")))
|
|
47 |
(global-set-key [?\s-j] '(lambda () (interactive) (insert "\261")))
|
|
48 |
(global-set-key [?\s-k] '(lambda () (interactive) (insert "\262")))
|
|
49 |
(global-set-key [?\s-l] '(lambda () (interactive) (insert "\263")))
|
|
50 |
(global-set-key [?\s-m] '(lambda () (interactive) (insert "\264")))
|
|
51 |
(global-set-key [?\s-n] '(lambda () (interactive) (insert "\265")))
|
|
52 |
(global-set-key [?\s-x] '(lambda () (interactive) (insert "\266")))
|
|
53 |
(global-set-key [?\s-p] '(lambda () (interactive) (insert "\267")))
|
|
54 |
(global-set-key [?\s-r] '(lambda () (interactive) (insert "\270")))
|
|
55 |
(global-set-key [?\s-s] '(lambda () (interactive) (insert "\271")))
|
|
56 |
(global-set-key [?\s-t] '(lambda () (interactive) (insert "\272")))
|
|
57 |
(global-set-key [?\s-f] '(lambda () (interactive) (insert "\273")))
|
|
58 |
(global-set-key [?\s-c] '(lambda () (interactive) (insert "\274")))
|
|
59 |
(global-set-key [?\s-q] '(lambda () (interactive) (insert "\275")))
|
|
60 |
(global-set-key [?\s-w] '(lambda () (interactive) (insert "\276")))
|
|
61 |
(global-set-key [?\H-n] '(lambda () (interactive) (insert "\277")))
|
|
62 |
(global-set-key [?\H-a] '(lambda () (interactive) (insert "\300")))
|
|
63 |
(global-set-key [?\H-o] '(lambda () (interactive) (insert "\301")))
|
|
64 |
(global-set-key [?\H-f] '(lambda () (interactive) (insert "\302")))
|
|
65 |
(global-set-key [?\H-t] '(lambda () (interactive) (insert "\303")))
|
|
66 |
(global-set-key [?\H-F] '(lambda () (interactive) (insert "\304")))
|
|
67 |
(global-set-key [C-f5] '(lambda () (interactive) (insert "\305")))
|
|
68 |
(global-set-key [C-f6] '(lambda () (interactive) (insert "\306")))
|
|
69 |
(global-set-key [C-f7] '(lambda () (interactive) (insert "\307")))
|
|
70 |
(global-set-key [C-f8] '(lambda () (interactive) (insert "\310")))
|
|
71 |
(global-set-key [C-f9] '(lambda () (interactive) (insert "\311")))
|
|
72 |
(global-set-key [C-f10] '(lambda () (interactive) (insert "\312")))
|
|
73 |
(global-set-key [C-f11] '(lambda () (interactive) (insert "\313")))
|
|
74 |
(global-set-key [C-f12] '(lambda () (interactive) (insert "\314")))
|
|
75 |
(global-set-key [H-f5] '(lambda () (interactive) (insert "\317")))
|
|
76 |
(global-set-key [H-f6] '(lambda () (interactive) (insert "\371")))
|
|
77 |
(global-set-key [H-f7] '(lambda () (interactive) (insert "\372")))
|
|
78 |
(global-set-key [H-f1] '(lambda () (interactive) (insert "\320")))
|
|
79 |
(global-set-key [H-f2] '(lambda () (interactive) (insert "\321")))
|
|
80 |
(global-set-key [H-f3] '(lambda () (interactive) (insert "\322")))
|
|
81 |
(global-set-key [H-f4] '(lambda () (interactive) (insert "\323")))
|
|
82 |
(global-set-key [C-f1] '(lambda () (interactive) (insert "\324")))
|
|
83 |
(global-set-key [C-f2] '(lambda () (interactive) (insert "\325")))
|
|
84 |
(global-set-key [C-f3] '(lambda () (interactive) (insert "\326")))
|
|
85 |
(global-set-key [C-f4] '(lambda () (interactive) (insert "\327")))
|
|
86 |
(global-set-key [?\H-b] '(lambda () (interactive) (insert "\330")))
|
|
87 |
(global-set-key [?\H-e] '(lambda () (interactive) (insert "\331")))
|
|
88 |
(global-set-key [?\H-E] '(lambda () (interactive) (insert "\332")))
|
|
89 |
(global-set-key [?\H-u] '(lambda () (interactive) (insert "\333")))
|
|
90 |
(global-set-key [?\H-p] '(lambda () (interactive) (insert "\334")))
|
|
91 |
(global-set-key [?\H-P] '(lambda () (interactive) (insert "\335")))
|
|
92 |
(global-set-key [?\H-l] '(lambda () (interactive) (insert "\336")))
|
|
93 |
(global-set-key [?\H-L] '(lambda () (interactive) (insert "\337")))
|
|
94 |
(global-set-key [?\H-g] '(lambda () (interactive) (insert "\340")))
|
|
95 |
(global-set-key [?\H-G] '(lambda () (interactive) (insert "\341")))
|
|
96 |
(global-set-key [?\H-s] '(lambda () (interactive) (insert "\342")))
|
|
97 |
(global-set-key [?\H-S] '(lambda () (interactive) (insert "\343")))
|
|
98 |
(global-set-key [S-f11] '(lambda () (interactive) (insert "\344")))
|
|
99 |
(global-set-key [S-f12] '(lambda () (interactive) (insert "\345")))
|
|
100 |
(global-set-key [s-f1] '(lambda () (interactive) (insert "\346")))
|
|
101 |
(global-set-key [s-f2] '(lambda () (interactive) (insert "\347")))
|
|
102 |
(global-set-key [s-f3] '(lambda () (interactive) (insert "\350")))
|
|
103 |
(global-set-key [S-f1] '(lambda () (interactive) (insert "\351")))
|
|
104 |
(global-set-key [S-f2] '(lambda () (interactive) (insert "\352")))
|
|
105 |
(global-set-key [S-f3] '(lambda () (interactive) (insert "\353")))
|
|
106 |
(global-set-key [s-f5] '(lambda () (interactive) (insert "\354")))
|
|
107 |
(global-set-key [s-f6] '(lambda () (interactive) (insert "\355")))
|
|
108 |
(global-set-key [s-f7] '(lambda () (interactive) (insert "\356")))
|
|
109 |
(global-set-key [s-f8] '(lambda () (interactive) (insert "\357")))
|
|
110 |
(global-set-key [s-f9] '(lambda () (interactive) (insert "\360")))
|
|
111 |
(global-set-key [s-f10] '(lambda () (interactive) (insert "\315")))
|
|
112 |
(global-set-key [?\H-x] '(lambda () (interactive) (insert "\362")))
|
|
113 |
(global-set-key [S-f5] '(lambda () (interactive) (insert "\363")))
|
|
114 |
(global-set-key [S-f6] '(lambda () (interactive) (insert "\364")))
|
|
115 |
(global-set-key [S-f7] '(lambda () (interactive) (insert "\365")))
|
|
116 |
(global-set-key [S-f8] '(lambda () (interactive) (insert "\366")))
|
|
117 |
(global-set-key [S-f9] '(lambda () (interactive) (insert "\367")))
|
|
118 |
(global-set-key [S-f10] '(lambda () (interactive) (insert "\370")))
|
|
119 |
(global-set-key [s-f11] '(lambda () (interactive) (insert "\316")))
|
|
120 |
(global-set-key [s-f12] '(lambda () (interactive) (insert "\361")))
|
|
121 |
(global-set-key [H-f8] '(lambda () (interactive) (insert "\373")))
|
|
122 |
(global-set-key [H-f9] '(lambda () (interactive) (insert "\374")))
|
|
123 |
(global-set-key [H-f10] '(lambda () (interactive) (insert "\375")))
|
|
124 |
(global-set-key [H-f11] '(lambda () (interactive) (insert "\376")))
|
|
125 |
(global-set-key [H-f12] '(lambda () (interactive) (insert "\377")))
|
|
126 |
(global-set-key [S-f4] '(lambda () (interactive) (insert "\351")(insert "\353")))
|
|
127 |
(global-set-key [s-f4] '(lambda () (interactive) (insert "\346")(insert "\350")))
|
|
128 |
(global-set-key [?\H-i] '(lambda () (interactive) (insert "\347")(insert "\350")))
|
|
129 |
(global-set-key [?\H-I] '(lambda () (interactive) (insert "\352")(insert "\353")))
|
|
130 |
(global-set-key [?\H-m] '(lambda () (interactive) (insert "\350")))
|
|
131 |
(global-set-key [?\H-M] '(lambda () (interactive) (insert "\353")))
|
|
132 |
(global-set-key [?\H-N] '(lambda () (interactive) (insert "\367")))
|
|
133 |
(global-set-key [f9] '(lambda () (interactive) (insert "\304")))
|
|
134 |
(global-set-key [f10] '(lambda () (interactive) (insert "\352")(insert "\353")))
|
|
135 |
(global-set-key [f11] '(lambda () (interactive) (insert "\332")))
|
|
136 |
(global-set-key [f12] '(lambda () (interactive) (insert "\333")))
|
|
137 |
;; END-KEY-MAP
|
|
138 |
)
|
|
139 |
(progn
|
|
140 |
(defun isabelle-fonts-menu (e)
|
|
141 |
"Pops up the Isabelle fonts menu."
|
|
142 |
(interactive "@e")
|
|
143 |
(popup-menu
|
|
144 |
'("Isabelle fonts menu"
|
|
145 |
["Isabelle 14" (set-face-font 'default "isabelle14") t]
|
|
146 |
["Isabelle 24" (set-face-font 'default "isabelle24") t])))
|
2938
|
147 |
|
3304
|
148 |
(global-unset-key '(shift control button3))
|
|
149 |
(global-set-key '(shift control button3) 'isabelle-fonts-menu)
|
|
150 |
|
|
151 |
;;FIXME
|
|
152 |
;; DO NOT EDIT the lines between BEGIN-KEY-MAP and END-KEY-MAP
|
|
153 |
;; the table is generated by the perl script `gen-isa_xemacs'
|
|
154 |
;; In order to make changes to the keyboard mappings you should edit
|
|
155 |
;; the configuration file `key-table.inp' which is interpreted by
|
|
156 |
;; the perl script `gen-isa_xemacs',
|
|
157 |
;;
|
|
158 |
;;
|
|
159 |
;; key-map for Isabelle font
|
|
160 |
;;
|
|
161 |
;; BEGIN-KEY-MAP
|
|
162 |
(global-set-key '(super G) '(lambda () (interactive) (insert "\241")))
|
|
163 |
(global-set-key '(super D) '(lambda () (interactive) (insert "\242")))
|
|
164 |
(global-set-key '(super J) '(lambda () (interactive) (insert "\243")))
|
|
165 |
(global-set-key '(super L) '(lambda () (interactive) (insert "\244")))
|
|
166 |
(global-set-key '(super P) '(lambda () (interactive) (insert "\245")))
|
|
167 |
(global-set-key '(super S) '(lambda () (interactive) (insert "\246")))
|
|
168 |
(global-set-key '(super F) '(lambda () (interactive) (insert "\247")))
|
|
169 |
(global-set-key '(super Q) '(lambda () (interactive) (insert "\250")))
|
|
170 |
(global-set-key '(super W) '(lambda () (interactive) (insert "\251")))
|
|
171 |
(global-set-key '(super a) '(lambda () (interactive) (insert "\252")))
|
|
172 |
(global-set-key '(super b) '(lambda () (interactive) (insert "\253")))
|
|
173 |
(global-set-key '(super g) '(lambda () (interactive) (insert "\254")))
|
|
174 |
(global-set-key '(super d) '(lambda () (interactive) (insert "\255")))
|
|
175 |
(global-set-key '(super e) '(lambda () (interactive) (insert "\256")))
|
|
176 |
(global-set-key '(super z) '(lambda () (interactive) (insert "\257")))
|
|
177 |
(global-set-key '(super h) '(lambda () (interactive) (insert "\260")))
|
|
178 |
(global-set-key '(super j) '(lambda () (interactive) (insert "\261")))
|
|
179 |
(global-set-key '(super k) '(lambda () (interactive) (insert "\262")))
|
|
180 |
(global-set-key '(super l) '(lambda () (interactive) (insert "\263")))
|
|
181 |
(global-set-key '(super m) '(lambda () (interactive) (insert "\264")))
|
|
182 |
(global-set-key '(super n) '(lambda () (interactive) (insert "\265")))
|
|
183 |
(global-set-key '(super x) '(lambda () (interactive) (insert "\266")))
|
|
184 |
(global-set-key '(super p) '(lambda () (interactive) (insert "\267")))
|
|
185 |
(global-set-key '(super r) '(lambda () (interactive) (insert "\270")))
|
|
186 |
(global-set-key '(super s) '(lambda () (interactive) (insert "\271")))
|
|
187 |
(global-set-key '(super t) '(lambda () (interactive) (insert "\272")))
|
|
188 |
(global-set-key '(super f) '(lambda () (interactive) (insert "\273")))
|
|
189 |
(global-set-key '(super c) '(lambda () (interactive) (insert "\274")))
|
|
190 |
(global-set-key '(super q) '(lambda () (interactive) (insert "\275")))
|
|
191 |
(global-set-key '(super w) '(lambda () (interactive) (insert "\276")))
|
|
192 |
(global-set-key '(hyper n) '(lambda () (interactive) (insert "\277")))
|
|
193 |
(global-set-key '(hyper a) '(lambda () (interactive) (insert "\300")))
|
|
194 |
(global-set-key '(hyper o) '(lambda () (interactive) (insert "\301")))
|
|
195 |
(global-set-key '(hyper f) '(lambda () (interactive) (insert "\302")))
|
|
196 |
(global-set-key '(hyper t) '(lambda () (interactive) (insert "\303")))
|
|
197 |
(global-set-key '(hyper F) '(lambda () (interactive) (insert "\304")))
|
|
198 |
(global-set-key '(control f5) '(lambda () (interactive) (insert "\305")))
|
|
199 |
(global-set-key '(control f6) '(lambda () (interactive) (insert "\306")))
|
|
200 |
(global-set-key '(control f7) '(lambda () (interactive) (insert "\307")))
|
|
201 |
(global-set-key '(control f8) '(lambda () (interactive) (insert "\310")))
|
|
202 |
(global-set-key '(control f9) '(lambda () (interactive) (insert "\311")))
|
|
203 |
(global-set-key '(control f10) '(lambda () (interactive) (insert "\312")))
|
|
204 |
(global-set-key '(control f11) '(lambda () (interactive) (insert "\313")))
|
|
205 |
(global-set-key '(control f12) '(lambda () (interactive) (insert "\314")))
|
|
206 |
(global-set-key '(hyper f5) '(lambda () (interactive) (insert "\317")))
|
|
207 |
(global-set-key '(hyper f6) '(lambda () (interactive) (insert "\371")))
|
|
208 |
(global-set-key '(hyper f7) '(lambda () (interactive) (insert "\372")))
|
|
209 |
(global-set-key '(hyper f1) '(lambda () (interactive) (insert "\320")))
|
|
210 |
(global-set-key '(hyper f2) '(lambda () (interactive) (insert "\321")))
|
|
211 |
(global-set-key '(hyper f3) '(lambda () (interactive) (insert "\322")))
|
|
212 |
(global-set-key '(hyper f4) '(lambda () (interactive) (insert "\323")))
|
|
213 |
(global-set-key '(control f1) '(lambda () (interactive) (insert "\324")))
|
|
214 |
(global-set-key '(control f2) '(lambda () (interactive) (insert "\325")))
|
|
215 |
(global-set-key '(control f3) '(lambda () (interactive) (insert "\326")))
|
|
216 |
(global-set-key '(control f4) '(lambda () (interactive) (insert "\327")))
|
|
217 |
(global-set-key '(hyper b) '(lambda () (interactive) (insert "\330")))
|
|
218 |
(global-set-key '(hyper e) '(lambda () (interactive) (insert "\331")))
|
|
219 |
(global-set-key '(hyper E) '(lambda () (interactive) (insert "\332")))
|
|
220 |
(global-set-key '(hyper u) '(lambda () (interactive) (insert "\333")))
|
|
221 |
(global-set-key '(hyper p) '(lambda () (interactive) (insert "\334")))
|
|
222 |
(global-set-key '(hyper P) '(lambda () (interactive) (insert "\335")))
|
|
223 |
(global-set-key '(hyper l) '(lambda () (interactive) (insert "\336")))
|
|
224 |
(global-set-key '(hyper L) '(lambda () (interactive) (insert "\337")))
|
|
225 |
(global-set-key '(hyper g) '(lambda () (interactive) (insert "\340")))
|
|
226 |
(global-set-key '(hyper G) '(lambda () (interactive) (insert "\341")))
|
|
227 |
(global-set-key '(hyper s) '(lambda () (interactive) (insert "\342")))
|
|
228 |
(global-set-key '(hyper S) '(lambda () (interactive) (insert "\343")))
|
|
229 |
(global-set-key '(shift f11) '(lambda () (interactive) (insert "\344")))
|
|
230 |
(global-set-key '(shift f12) '(lambda () (interactive) (insert "\345")))
|
|
231 |
(global-set-key '(super f1) '(lambda () (interactive) (insert "\346")))
|
|
232 |
(global-set-key '(super f2) '(lambda () (interactive) (insert "\347")))
|
|
233 |
(global-set-key '(super f3) '(lambda () (interactive) (insert "\350")))
|
|
234 |
(global-set-key '(shift f1) '(lambda () (interactive) (insert "\351")))
|
|
235 |
(global-set-key '(shift f2) '(lambda () (interactive) (insert "\352")))
|
|
236 |
(global-set-key '(shift f3) '(lambda () (interactive) (insert "\353")))
|
|
237 |
(global-set-key '(super f5) '(lambda () (interactive) (insert "\354")))
|
|
238 |
(global-set-key '(super f6) '(lambda () (interactive) (insert "\355")))
|
|
239 |
(global-set-key '(super f7) '(lambda () (interactive) (insert "\356")))
|
|
240 |
(global-set-key '(super f8) '(lambda () (interactive) (insert "\357")))
|
|
241 |
(global-set-key '(super f9) '(lambda () (interactive) (insert "\360")))
|
|
242 |
(global-set-key '(super f10) '(lambda () (interactive) (insert "\315")))
|
|
243 |
(global-set-key '(hyper x) '(lambda () (interactive) (insert "\362")))
|
|
244 |
(global-set-key '(shift f5) '(lambda () (interactive) (insert "\363")))
|
|
245 |
(global-set-key '(shift f6) '(lambda () (interactive) (insert "\364")))
|
|
246 |
(global-set-key '(shift f7) '(lambda () (interactive) (insert "\365")))
|
|
247 |
(global-set-key '(shift f8) '(lambda () (interactive) (insert "\366")))
|
|
248 |
(global-set-key '(shift f9) '(lambda () (interactive) (insert "\367")))
|
|
249 |
(global-set-key '(shift f10) '(lambda () (interactive) (insert "\370")))
|
|
250 |
(global-set-key '(super f11) '(lambda () (interactive) (insert "\316")))
|
|
251 |
(global-set-key '(super f12) '(lambda () (interactive) (insert "\361")))
|
|
252 |
(global-set-key '(hyper f8) '(lambda () (interactive) (insert "\373")))
|
|
253 |
(global-set-key '(hyper f9) '(lambda () (interactive) (insert "\374")))
|
|
254 |
(global-set-key '(hyper f10) '(lambda () (interactive) (insert "\375")))
|
|
255 |
(global-set-key '(hyper f11) '(lambda () (interactive) (insert "\376")))
|
|
256 |
(global-set-key '(hyper f12) '(lambda () (interactive) (insert "\377")))
|
|
257 |
(global-set-key '(shift f4) '(lambda () (interactive) (insert "\351")(insert "\353")))
|
|
258 |
(global-set-key '(super f4) '(lambda () (interactive) (insert "\346")(insert "\350")))
|
|
259 |
(global-set-key '(hyper i) '(lambda () (interactive) (insert "\347")(insert "\350")))
|
|
260 |
(global-set-key '(hyper I) '(lambda () (interactive) (insert "\352")(insert "\353")))
|
|
261 |
(global-set-key '(hyper m) '(lambda () (interactive) (insert "\350")))
|
|
262 |
(global-set-key '(hyper M) '(lambda () (interactive) (insert "\353")))
|
|
263 |
(global-set-key '(hyper N) '(lambda () (interactive) (insert "\367")))
|
|
264 |
(global-set-key '(f9) '(lambda () (interactive) (insert "\304")))
|
|
265 |
(global-set-key '(f10) '(lambda () (interactive) (insert "\352")(insert "\353")))
|
|
266 |
(global-set-key '(f11) '(lambda () (interactive) (insert "\332")))
|
|
267 |
(global-set-key '(f12) '(lambda () (interactive) (insert "\333")))
|
|
268 |
;; END-KEY-MAP
|
|
269 |
))
|