| 1826 |      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
 | 
| 2833 |     14 | (set-default-font "isabelle14")
 | 
| 1826 |     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.
 | 
| 2833 |     28 | ("14 isabelle " "isabelle14")
 | 
|  |     29 | ("24 isabelle " "isabelle24")
 | 
| 1826 |     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
 | 
| 4638 |     43 | (global-set-key [s-space] '(lambda () (interactive) (insert "\240")))
 | 
| 1826 |     44 | (global-set-key [?\s-G] '(lambda () (interactive) (insert "\241")))
 | 
|  |     45 | (global-set-key [?\s-D] '(lambda () (interactive) (insert "\242")))
 | 
|  |     46 | (global-set-key [?\s-J] '(lambda () (interactive) (insert "\243")))
 | 
|  |     47 | (global-set-key [?\s-L] '(lambda () (interactive) (insert "\244")))
 | 
|  |     48 | (global-set-key [?\s-P] '(lambda () (interactive) (insert "\245")))
 | 
|  |     49 | (global-set-key [?\s-S] '(lambda () (interactive) (insert "\246")))
 | 
|  |     50 | (global-set-key [?\s-F] '(lambda () (interactive) (insert "\247")))
 | 
|  |     51 | (global-set-key [?\s-Q] '(lambda () (interactive) (insert "\250")))
 | 
|  |     52 | (global-set-key [?\s-W] '(lambda () (interactive) (insert "\251")))
 | 
|  |     53 | (global-set-key [?\s-a] '(lambda () (interactive) (insert "\252")))
 | 
|  |     54 | (global-set-key [?\s-b] '(lambda () (interactive) (insert "\253")))
 | 
|  |     55 | (global-set-key [?\s-g] '(lambda () (interactive) (insert "\254")))
 | 
|  |     56 | (global-set-key [?\s-d] '(lambda () (interactive) (insert "\255")))
 | 
|  |     57 | (global-set-key [?\s-e] '(lambda () (interactive) (insert "\256")))
 | 
|  |     58 | (global-set-key [?\s-z] '(lambda () (interactive) (insert "\257")))
 | 
|  |     59 | (global-set-key [?\s-h] '(lambda () (interactive) (insert "\260")))
 | 
|  |     60 | (global-set-key [?\s-j] '(lambda () (interactive) (insert "\261")))
 | 
|  |     61 | (global-set-key [?\s-k] '(lambda () (interactive) (insert "\262")))
 | 
|  |     62 | (global-set-key [?\s-l] '(lambda () (interactive) (insert "\263")))
 | 
|  |     63 | (global-set-key [?\s-m] '(lambda () (interactive) (insert "\264")))
 | 
|  |     64 | (global-set-key [?\s-n] '(lambda () (interactive) (insert "\265")))
 | 
|  |     65 | (global-set-key [?\s-x] '(lambda () (interactive) (insert "\266")))
 | 
|  |     66 | (global-set-key [?\s-p] '(lambda () (interactive) (insert "\267")))
 | 
|  |     67 | (global-set-key [?\s-r] '(lambda () (interactive) (insert "\270")))
 | 
|  |     68 | (global-set-key [?\s-s] '(lambda () (interactive) (insert "\271")))
 | 
|  |     69 | (global-set-key [?\s-t] '(lambda () (interactive) (insert "\272")))
 | 
|  |     70 | (global-set-key [?\s-f] '(lambda () (interactive) (insert "\273")))
 | 
|  |     71 | (global-set-key [?\s-c] '(lambda () (interactive) (insert "\274")))
 | 
|  |     72 | (global-set-key [?\s-q] '(lambda () (interactive) (insert "\275")))
 | 
|  |     73 | (global-set-key [?\s-w] '(lambda () (interactive) (insert "\276")))
 | 
|  |     74 | (global-set-key [?\H-n] '(lambda () (interactive) (insert "\277")))
 | 
|  |     75 | (global-set-key [?\H-a] '(lambda () (interactive) (insert "\300")))
 | 
|  |     76 | (global-set-key [?\H-o] '(lambda () (interactive) (insert "\301")))
 | 
|  |     77 | (global-set-key [?\H-f] '(lambda () (interactive) (insert "\302")))
 | 
|  |     78 | (global-set-key [?\H-t] '(lambda () (interactive) (insert "\303")))
 | 
|  |     79 | (global-set-key [?\H-F] '(lambda () (interactive) (insert "\304")))
 | 
|  |     80 | (global-set-key [?\H-b] '(lambda () (interactive) (insert "\330")))
 | 
|  |     81 | (global-set-key [?\H-e] '(lambda () (interactive) (insert "\331")))
 | 
|  |     82 | (global-set-key [?\H-E] '(lambda () (interactive) (insert "\332")))
 | 
|  |     83 | (global-set-key [?\H-u] '(lambda () (interactive) (insert "\333")))
 | 
|  |     84 | (global-set-key [?\H-p] '(lambda () (interactive) (insert "\334")))
 | 
|  |     85 | (global-set-key [?\H-P] '(lambda () (interactive) (insert "\335")))
 | 
|  |     86 | (global-set-key [?\H-l] '(lambda () (interactive) (insert "\336")))
 | 
|  |     87 | (global-set-key [?\H-L] '(lambda () (interactive) (insert "\337")))
 | 
|  |     88 | (global-set-key [?\H-g] '(lambda () (interactive) (insert "\340")))
 | 
|  |     89 | (global-set-key [?\H-G] '(lambda () (interactive) (insert "\341")))
 | 
|  |     90 | (global-set-key [?\H-s] '(lambda () (interactive) (insert "\342")))
 | 
|  |     91 | (global-set-key [?\H-S] '(lambda () (interactive) (insert "\343")))
 | 
| 4638 |     92 | (global-set-key [?\H-i] '(lambda () (interactive) (insert "\347")(insert "\350")))
 | 
|  |     93 | (global-set-key [?\H-I] '(lambda () (interactive) (insert "\352")(insert "\353")))
 | 
|  |     94 | (global-set-key [?\H-M] '(lambda () (interactive) (insert "\350")))
 | 
|  |     95 | (global-set-key [?\H-m] '(lambda () (interactive) (insert "\353")))
 | 
|  |     96 | (global-set-key [?\H-N] '(lambda () (interactive) (insert "\367")))
 | 
|  |     97 | (global-set-key [?\H-x] '(lambda () (interactive) (insert "\362")))
 | 
|  |     98 | (global-set-key [f2] '(lambda () (interactive) (insert "\344")))
 | 
|  |     99 | (global-set-key [f3] '(lambda () (interactive) (insert "\335")))
 | 
|  |    100 | (global-set-key [f4] '(lambda () (interactive) (insert "\317")))
 | 
|  |    101 | (global-set-key [f5] '(lambda () (interactive) (insert "\316")))
 | 
|  |    102 | (global-set-key [f6] '(lambda () (interactive) (insert "\361")))
 | 
|  |    103 | (global-set-key [f7] '(lambda () (interactive) (insert "\345")))
 | 
|  |    104 | (global-set-key [f8] '(lambda () (interactive) (insert "\332")))
 | 
|  |    105 | (global-set-key [f9] '(lambda () (interactive) (insert "\304")))
 | 
|  |    106 | (global-set-key [f10] '(lambda () (interactive) (insert "\313")))
 | 
|  |    107 | (global-set-key [f11] '(lambda () (interactive) (insert "\314")))
 | 
|  |    108 | (global-set-key [f12] '(lambda () (interactive) (insert "\352")(insert "\353")))
 | 
| 1826 |    109 | (global-set-key [S-f1] '(lambda () (interactive) (insert "\351")))
 | 
|  |    110 | (global-set-key [S-f2] '(lambda () (interactive) (insert "\352")))
 | 
|  |    111 | (global-set-key [S-f3] '(lambda () (interactive) (insert "\353")))
 | 
| 4638 |    112 | (global-set-key [S-f4] '(lambda () (interactive) (insert "\351")(insert "\353")))
 | 
| 1826 |    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")))
 | 
| 4638 |    117 | (global-set-key [S-f9] '(lambda () (interactive) (insert "\312")))
 | 
|  |    118 | (global-set-key [S-f10] '(lambda () (interactive) (insert "\311")))
 | 
|  |    119 | (global-set-key [C-f1] '(lambda () (interactive) (insert "\346")))
 | 
|  |    120 | (global-set-key [C-f2] '(lambda () (interactive) (insert "\347")))
 | 
|  |    121 | (global-set-key [C-f3] '(lambda () (interactive) (insert "\350")))
 | 
|  |    122 | (global-set-key [C-f4] '(lambda () (interactive) (insert "\346")(insert "\350")))
 | 
|  |    123 | (global-set-key [C-f5] '(lambda () (interactive) (insert "\305")))
 | 
|  |    124 | (global-set-key [C-f6] '(lambda () (interactive) (insert "\306")))
 | 
|  |    125 | (global-set-key [C-f7] '(lambda () (interactive) (insert "\307")))
 | 
|  |    126 | (global-set-key [C-f8] '(lambda () (interactive) (insert "\310")))
 | 
|  |    127 | (global-set-key [C-f9] '(lambda () (interactive) (insert "\375")))
 | 
|  |    128 | (global-set-key [C-f10] '(lambda () (interactive) (insert "\315")))
 | 
|  |    129 | (global-set-key [s-f1] '(lambda () (interactive) (insert "\355")))
 | 
|  |    130 | (global-set-key [s-f2] '(lambda () (interactive) (insert "\356")))
 | 
|  |    131 | (global-set-key [s-f3] '(lambda () (interactive) (insert "\357")))
 | 
|  |    132 | (global-set-key [s-f4] '(lambda () (interactive) (insert "\360")))
 | 
|  |    133 | (global-set-key [s-f5] '(lambda () (interactive) (insert "\324")))
 | 
|  |    134 | (global-set-key [s-f6] '(lambda () (interactive) (insert "\325")))
 | 
|  |    135 | (global-set-key [s-f7] '(lambda () (interactive) (insert "\326")))
 | 
|  |    136 | (global-set-key [s-f8] '(lambda () (interactive) (insert "\327")))
 | 
|  |    137 | (global-set-key [s-f9] '(lambda () (interactive) (insert "\334")))
 | 
|  |    138 | (global-set-key [s-f10] '(lambda () (interactive) (insert "\370")))
 | 
|  |    139 | (global-set-key [H-f1] '(lambda () (interactive) (insert "\371")))
 | 
|  |    140 | (global-set-key [H-f2] '(lambda () (interactive) (insert "\372")))
 | 
|  |    141 | (global-set-key [H-f3] '(lambda () (interactive) (insert "\373")))
 | 
|  |    142 | (global-set-key [H-f4] '(lambda () (interactive) (insert "\374")))
 | 
|  |    143 | (global-set-key [H-f5] '(lambda () (interactive) (insert "\320")))
 | 
|  |    144 | (global-set-key [H-f6] '(lambda () (interactive) (insert "\321")))
 | 
|  |    145 | (global-set-key [H-f7] '(lambda () (interactive) (insert "\322")))
 | 
|  |    146 | (global-set-key [H-f8] '(lambda () (interactive) (insert "\323")))
 | 
|  |    147 | (global-set-key [H-f9] '(lambda () (interactive) (insert "\367")))
 | 
|  |    148 | (global-set-key [H-f10] '(lambda () (interactive) (insert "\354")))
 | 
| 1826 |    149 | (global-set-key [H-f11] '(lambda () (interactive) (insert "\376")))
 | 
|  |    150 | (global-set-key [H-f12] '(lambda () (interactive) (insert "\377")))
 | 
|  |    151 | ;; END-KEY-MAP
 | 
|  |    152 | 
 | 
|  |    153 | 
 |