src/Tools/8bit/gnu_emacs/.emacs_isa_gnu_emacs

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 
;; Default parameters for emacs 19.27.1

;;   activate 8bit chars 
;;   ...for all new buffers
(setq default-ctl-arrow "z")
;;   ...and for the still active buffer
(setq ctl-arrow "z")
;;  Switch to ISO display
;(standard-display-european 1)
;(require 'iso-syntax)


(setq default-frame-alist  
        '(
        (font . "isabelle14")
        (icon-type . t) 
        (menu-bar-lines . 1)
        (width . 80)
        (height . 30)
        ))

(transient-mark-mode 1)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; MOUSE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(global-unset-key [mouse-3])
(global-set-key [mouse-3]  'kill-region)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; some defaults 

(setq-default case-fold-search nil)
(setq fill-column 64)

(setq text-mode-hook 'turn-on-auto-fill)

(setq make-backup-files nil)
(put 'eval-expression 'disabled nil)
(setq auto-mode-alist (mapcar 'purecopy
                              '(("\\.c$" . c-mode)
                                ("\\.h$" . c-mode)
                                ("\\.tex$" . TeX-mode)
                                ("\\.itex$" . TeX-mode)
                                ("\\.txi$" . Texinfo-mode)
                                ("\\.el$" . emacs-lisp-mode)
                                ("\\.a$" . c-mode))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Note:  C-c <letter> sequences are reserved for users own bindings
;;
 
(defun Ctl-C-prefix ()                  ; Use Ctl-C as a command prefix
  Ctl-C-keymap)
(setq Ctl-C-keymap (make-keymap))       ; allocate Ctl-C keymap table
(global-set-key "\C-c" (Ctl-C-prefix))  ; define Ctl-C function
 
(define-key Ctl-C-keymap "g" 'goto-line)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; define an alternate keymap
;;

(defvar cursor-map-2 (make-keymap) "for ESC-[")
(fset 'Cursor-Map-2 cursor-map-2)
(define-key esc-map "[" 'Cursor-Map-2)
 
(define-key esc-map "[[B" 'byte-compile-file)
(define-key esc-map "[[E" 'eval-defun)
(define-key esc-map "[[F" 'eval-current-buffer)
(define-key esc-map "[[G" 'eval-region)
(define-key esc-map "[[L" 'load-file)
(define-key esc-map "[[R" 'replace-regexp)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;               AUC - TeX
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(require 'tex-site)
(setq TeX-auto-global nil)
(setq TeX-auto-local nil)
(setq-default TeX-parse-self nil)
(setq-default TeX-auto-save nil)
 
(setq LaTeX-default-options "german,a4,12pt")
(setq TeX-auto-untabify  nil)

(setq LaTeX-mode-hook '(lambda () (local-unset-key  "\"")
                                  (auto-fill-mode 1)
))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                 ispell
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(setq ispell-highlight-face 'modeline)
 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                 ISABELLE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(load-file "goalify.el")
(define-key Ctl-C-keymap "G" 'goalify)
(define-key Ctl-C-keymap "U" 'ungoalify)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                 ISABELLE to LaTeX
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-key Ctl-C-keymap "i" '(lambda () (interactive) (insert "\\I@isa")))
(define-key Ctl-C-keymap "a" '(lambda () (interactive) (insert "\\I@")))
(define-key Ctl-C-keymap "e" '(lambda () (interactive) (insert "\\E@")))

(define-key Ctl-C-keymap "t" '(lambda () (interactive) (insert "\t")))