|
1 ;; |
|
2 ;; -- init-file for GNU Emacs for Isabelle environment |
|
3 ;; |
|
4 ;; derived from |
|
5 ;; sgemacs by Ralf S. Engelschall, <rse@en.muc.de> |
|
6 ;; |
|
7 ;; added isabelle fonts to font-selection menu |
|
8 ;; the key-map is now generated by a perl script |
|
9 ;; Franz Regensburger <regensbu@informatik.tu-muenchen.de> |
|
10 ;; 22.03.95 |
|
11 ;; |
|
12 |
|
13 ;;; Isabelle font as default |
|
14 (set-default-font "isacr14") |
|
15 |
|
16 ;; activate 8bit chars |
|
17 ;; ...for all new buffers |
|
18 (setq default-ctl-arrow "z") |
|
19 ;; ...and for the still active buffer |
|
20 (setq ctl-arrow "z") |
|
21 ;; Switch to ISO display |
|
22 (standard-display-european 1) |
|
23 (require 'iso-syntax) |
|
24 |
|
25 (setcdr x-fixed-font-alist |
|
26 (cons '("Symbol fonts" |
|
27 ;; These are the available isabelle and spectrum fonts. |
|
28 ("14 isabelle " "isacr14") |
|
29 ("24 isabelle " "isacb24") |
|
30 ) |
|
31 (cdr x-fixed-font-alist))) |
|
32 |
|
33 ;; DO NOT EDIT the lines between BEGIN-KEY-MAP and END-KEY-MAP |
|
34 ;; the table is generated by the perl script `gen-isa_gnu_emacs' |
|
35 ;; In order to make changes to the keyboard mappings you should edit |
|
36 ;; the configuration file `key-table.inp' which is interpreted by |
|
37 ;; the perl script `gen-isa_gnu_emacs', |
|
38 ;; |
|
39 ;; |
|
40 ;; key-map for Isabelle font |
|
41 ;; |
|
42 ;; BEGIN-KEY-MAP |
|
43 (global-set-key [?\s-G] '(lambda () (interactive) (insert "\241"))) |
|
44 (global-set-key [?\s-D] '(lambda () (interactive) (insert "\242"))) |
|
45 (global-set-key [?\s-J] '(lambda () (interactive) (insert "\243"))) |
|
46 (global-set-key [?\s-L] '(lambda () (interactive) (insert "\244"))) |
|
47 (global-set-key [?\s-P] '(lambda () (interactive) (insert "\245"))) |
|
48 (global-set-key [?\s-S] '(lambda () (interactive) (insert "\246"))) |
|
49 (global-set-key [?\s-F] '(lambda () (interactive) (insert "\247"))) |
|
50 (global-set-key [?\s-Q] '(lambda () (interactive) (insert "\250"))) |
|
51 (global-set-key [?\s-W] '(lambda () (interactive) (insert "\251"))) |
|
52 (global-set-key [?\s-a] '(lambda () (interactive) (insert "\252"))) |
|
53 (global-set-key [?\s-b] '(lambda () (interactive) (insert "\253"))) |
|
54 (global-set-key [?\s-g] '(lambda () (interactive) (insert "\254"))) |
|
55 (global-set-key [?\s-d] '(lambda () (interactive) (insert "\255"))) |
|
56 (global-set-key [?\s-e] '(lambda () (interactive) (insert "\256"))) |
|
57 (global-set-key [?\s-z] '(lambda () (interactive) (insert "\257"))) |
|
58 (global-set-key [?\s-h] '(lambda () (interactive) (insert "\260"))) |
|
59 (global-set-key [?\s-j] '(lambda () (interactive) (insert "\261"))) |
|
60 (global-set-key [?\s-k] '(lambda () (interactive) (insert "\262"))) |
|
61 (global-set-key [?\s-l] '(lambda () (interactive) (insert "\263"))) |
|
62 (global-set-key [?\s-m] '(lambda () (interactive) (insert "\264"))) |
|
63 (global-set-key [?\s-n] '(lambda () (interactive) (insert "\265"))) |
|
64 (global-set-key [?\s-x] '(lambda () (interactive) (insert "\266"))) |
|
65 (global-set-key [?\s-p] '(lambda () (interactive) (insert "\267"))) |
|
66 (global-set-key [?\s-r] '(lambda () (interactive) (insert "\270"))) |
|
67 (global-set-key [?\s-s] '(lambda () (interactive) (insert "\271"))) |
|
68 (global-set-key [?\s-t] '(lambda () (interactive) (insert "\272"))) |
|
69 (global-set-key [?\s-f] '(lambda () (interactive) (insert "\273"))) |
|
70 (global-set-key [?\s-c] '(lambda () (interactive) (insert "\274"))) |
|
71 (global-set-key [?\s-q] '(lambda () (interactive) (insert "\275"))) |
|
72 (global-set-key [?\s-w] '(lambda () (interactive) (insert "\276"))) |
|
73 (global-set-key [?\H-n] '(lambda () (interactive) (insert "\277"))) |
|
74 (global-set-key [?\H-a] '(lambda () (interactive) (insert "\300"))) |
|
75 (global-set-key [?\H-o] '(lambda () (interactive) (insert "\301"))) |
|
76 (global-set-key [?\H-f] '(lambda () (interactive) (insert "\302"))) |
|
77 (global-set-key [?\H-t] '(lambda () (interactive) (insert "\303"))) |
|
78 (global-set-key [?\H-F] '(lambda () (interactive) (insert "\304"))) |
|
79 (global-set-key [C-f5] '(lambda () (interactive) (insert "\305"))) |
|
80 (global-set-key [C-f6] '(lambda () (interactive) (insert "\306"))) |
|
81 (global-set-key [C-f7] '(lambda () (interactive) (insert "\307"))) |
|
82 (global-set-key [C-f8] '(lambda () (interactive) (insert "\310"))) |
|
83 (global-set-key [C-f9] '(lambda () (interactive) (insert "\311"))) |
|
84 (global-set-key [C-f10] '(lambda () (interactive) (insert "\312"))) |
|
85 (global-set-key [C-f11] '(lambda () (interactive) (insert "\313"))) |
|
86 (global-set-key [C-f12] '(lambda () (interactive) (insert "\314"))) |
|
87 (global-set-key [H-f5] '(lambda () (interactive) (insert "\317"))) |
|
88 (global-set-key [H-f6] '(lambda () (interactive) (insert "\371"))) |
|
89 (global-set-key [H-f7] '(lambda () (interactive) (insert "\372"))) |
|
90 (global-set-key [H-f1] '(lambda () (interactive) (insert "\320"))) |
|
91 (global-set-key [H-f2] '(lambda () (interactive) (insert "\321"))) |
|
92 (global-set-key [H-f3] '(lambda () (interactive) (insert "\322"))) |
|
93 (global-set-key [H-f4] '(lambda () (interactive) (insert "\323"))) |
|
94 (global-set-key [C-f1] '(lambda () (interactive) (insert "\324"))) |
|
95 (global-set-key [C-f2] '(lambda () (interactive) (insert "\325"))) |
|
96 (global-set-key [C-f3] '(lambda () (interactive) (insert "\326"))) |
|
97 (global-set-key [C-f4] '(lambda () (interactive) (insert "\327"))) |
|
98 (global-set-key [?\H-b] '(lambda () (interactive) (insert "\330"))) |
|
99 (global-set-key [?\H-e] '(lambda () (interactive) (insert "\331"))) |
|
100 (global-set-key [?\H-E] '(lambda () (interactive) (insert "\332"))) |
|
101 (global-set-key [?\H-u] '(lambda () (interactive) (insert "\333"))) |
|
102 (global-set-key [?\H-p] '(lambda () (interactive) (insert "\334"))) |
|
103 (global-set-key [?\H-P] '(lambda () (interactive) (insert "\335"))) |
|
104 (global-set-key [?\H-l] '(lambda () (interactive) (insert "\336"))) |
|
105 (global-set-key [?\H-L] '(lambda () (interactive) (insert "\337"))) |
|
106 (global-set-key [?\H-g] '(lambda () (interactive) (insert "\340"))) |
|
107 (global-set-key [?\H-G] '(lambda () (interactive) (insert "\341"))) |
|
108 (global-set-key [?\H-s] '(lambda () (interactive) (insert "\342"))) |
|
109 (global-set-key [?\H-S] '(lambda () (interactive) (insert "\343"))) |
|
110 (global-set-key [S-f11] '(lambda () (interactive) (insert "\344"))) |
|
111 (global-set-key [S-f12] '(lambda () (interactive) (insert "\345"))) |
|
112 (global-set-key [s-f1] '(lambda () (interactive) (insert "\346"))) |
|
113 (global-set-key [s-f2] '(lambda () (interactive) (insert "\347"))) |
|
114 (global-set-key [s-f3] '(lambda () (interactive) (insert "\350"))) |
|
115 (global-set-key [S-f1] '(lambda () (interactive) (insert "\351"))) |
|
116 (global-set-key [S-f2] '(lambda () (interactive) (insert "\352"))) |
|
117 (global-set-key [S-f3] '(lambda () (interactive) (insert "\353"))) |
|
118 (global-set-key [s-f5] '(lambda () (interactive) (insert "\354"))) |
|
119 (global-set-key [s-f6] '(lambda () (interactive) (insert "\355"))) |
|
120 (global-set-key [s-f7] '(lambda () (interactive) (insert "\356"))) |
|
121 (global-set-key [s-f8] '(lambda () (interactive) (insert "\357"))) |
|
122 (global-set-key [s-f9] '(lambda () (interactive) (insert "\360"))) |
|
123 (global-set-key [s-f10] '(lambda () (interactive) (insert "\315"))) |
|
124 (global-set-key [?\H-x] '(lambda () (interactive) (insert "\362"))) |
|
125 (global-set-key [S-f5] '(lambda () (interactive) (insert "\363"))) |
|
126 (global-set-key [S-f6] '(lambda () (interactive) (insert "\364"))) |
|
127 (global-set-key [S-f7] '(lambda () (interactive) (insert "\365"))) |
|
128 (global-set-key [S-f8] '(lambda () (interactive) (insert "\366"))) |
|
129 (global-set-key [S-f9] '(lambda () (interactive) (insert "\367"))) |
|
130 (global-set-key [S-f10] '(lambda () (interactive) (insert "\370"))) |
|
131 (global-set-key [s-f11] '(lambda () (interactive) (insert "\316"))) |
|
132 (global-set-key [s-f12] '(lambda () (interactive) (insert "\361"))) |
|
133 (global-set-key [H-f8] '(lambda () (interactive) (insert "\373"))) |
|
134 (global-set-key [H-f9] '(lambda () (interactive) (insert "\374"))) |
|
135 (global-set-key [H-f10] '(lambda () (interactive) (insert "\375"))) |
|
136 (global-set-key [H-f11] '(lambda () (interactive) (insert "\376"))) |
|
137 (global-set-key [H-f12] '(lambda () (interactive) (insert "\377"))) |
|
138 (global-set-key [S-f4] '(lambda () (interactive) (insert "\351")(insert "\353"))) |
|
139 (global-set-key [s-f4] '(lambda () (interactive) (insert "\346")(insert "\350"))) |
|
140 (global-set-key [?\H-i] '(lambda () (interactive) (insert "\347")(insert "\350"))) |
|
141 (global-set-key [?\H-I] '(lambda () (interactive) (insert "\352")(insert "\353"))) |
|
142 (global-set-key [?\H-m] '(lambda () (interactive) (insert "\350"))) |
|
143 (global-set-key [?\H-M] '(lambda () (interactive) (insert "\353"))) |
|
144 (global-set-key [?\H-N] '(lambda () (interactive) (insert "\367"))) |
|
145 (global-set-key [f9] '(lambda () (interactive) (insert "\304"))) |
|
146 (global-set-key [f10] '(lambda () (interactive) (insert "\352")(insert "\353"))) |
|
147 (global-set-key [f11] '(lambda () (interactive) (insert "\332"))) |
|
148 (global-set-key [f12] '(lambda () (interactive) (insert "\333"))) |
|
149 ;; END-KEY-MAP |
|
150 |
|
151 |