summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRené 'Necoro' Neumann <necoro@necoro.net>2012-09-04 23:48:01 +0200
committerRené 'Necoro' Neumann <necoro@necoro.net>2012-09-04 23:48:01 +0200
commitc43330157961612a211e16d4381ae536d15370fa (patch)
treee534f1ed70a953970f36c4712efa968cb1b7a2d6
parent6d7a29af83b339d73a66d35ae1216263e3631f03 (diff)
downloaddotfiles-c43330157961612a211e16d4381ae536d15370fa.tar.gz
dotfiles-c43330157961612a211e16d4381ae536d15370fa.tar.bz2
dotfiles-c43330157961612a211e16d4381ae536d15370fa.zip
More emacs/isabelle hacks
-rw-r--r--.emacs17
-rw-r--r--.emacs.d/custom.el16
-rw-r--r--.emacs.d/evil-settings.el11
3 files changed, 33 insertions, 11 deletions
diff --git a/.emacs b/.emacs
index 9ce4988..7918b26 100644
--- a/.emacs
+++ b/.emacs
@@ -29,6 +29,23 @@
;; use Poly/ML as SML interpreter
(setq sml-program-name "poly")
+;; work around two bugs in Isabelle/PG
+;; we need to toggle two options twice to make them work
+(defun repair-auto-solve ()
+ (when isar-tracing:auto-solve-direct
+ (print "Repairing Auto Solve Direct")
+ (isar-tracing:auto-solve-direct-toggle 0)
+ (isar-tracing:auto-solve-direct-toggle 1)))
+
+(defun repair-auto-quickcheck ()
+ (when isar-tracing:auto-quickcheck
+ (print "Repairing Auto Quickcheck")
+ (isar-tracing:auto-quickcheck-toggle 0)
+ (isar-tracing:auto-quickcheck-toggle 1)))
+
+(add-hook 'proof-shell-init-hook 'repair-auto-solve)
+(add-hook 'proof-shell-init-hook 'repair-auto-quickcheck)
+
;; custom file
(setq custom-file "~/.emacs.d/custom.el")
(load custom-file)
diff --git a/.emacs.d/custom.el b/.emacs.d/custom.el
index f103960..b0eac92 100644
--- a/.emacs.d/custom.el
+++ b/.emacs.d/custom.el
@@ -1,8 +1,8 @@
(custom-set-variables
- ;; custom-set-variables was added by Custom.
- ;; If you edit it by hand, you could mess it up, so be careful.
- ;; Your init file should contain only one such instance.
- ;; If there is more than one, they won't work right.
+ ;; custom-set-variables was added by Custom.
+ ;; If you edit it by hand, you could mess it up, so be careful.
+ ;; Your init file should contain only one such instance.
+ ;; If there is more than one, they won't work right.
'(indent-tabs-mode nil)
'(isar-display:show-main-goal t)
'(isar-maths-menu-enable t)
@@ -19,10 +19,10 @@
'(proof-three-window-enable t)
'(show-paren-mode t))
(custom-set-faces
- ;; custom-set-faces was added by Custom.
- ;; If you edit it by hand, you could mess it up, so be careful.
- ;; Your init file should contain only one such instance.
- ;; If there is more than one, they won't work right.
+ ;; custom-set-faces was added by Custom.
+ ;; If you edit it by hand, you could mess it up, so be careful.
+ ;; Your init file should contain only one such instance.
+ ;; If there is more than one, they won't work right.
'(default ((t (:inherit nil :stipple nil :background "Grey15" :foreground "Grey" :inverse-video nil :box nil :strike-through nil :overline nil :underline nil :slant normal :weight normal :height 113 :width normal :foundry "unknown" :family "Inconsolata"))))
'(isabelle-free-name-face ((((type x) (class color) (background dark)) (:foreground "lightblue"))))
'(isabelle-quote-face ((t (:foreground "grey21"))))
diff --git a/.emacs.d/evil-settings.el b/.emacs.d/evil-settings.el
index b646cf6..90d0396 100644
--- a/.emacs.d/evil-settings.el
+++ b/.emacs.d/evil-settings.el
@@ -11,6 +11,11 @@
(define-key evil-normal-state-map "Y" 'evil-yank-line-end)
; make unicode-tokens work
-(eval-after-load "isar" '(progn
- (unicode-tokens-use-shortcuts 0)
- (unicode-tokens-use-shortcuts 1)))
+(setq repair-unicode-shortcuts
+ '(progn
+ (print "Repairing Unicode Shortcuts for Evil")
+ (unicode-tokens-use-shortcuts 0)
+ (unicode-tokens-use-shortcuts 1)))
+
+(eval-after-load 'isar repair-unicode-shortcuts)
+