diff options
author | René 'Necoro' Neumann <necoro@necoro.net> | 2012-09-05 10:31:13 +0200 |
---|---|---|
committer | René 'Necoro' Neumann <necoro@necoro.net> | 2012-09-05 10:31:14 +0200 |
commit | 8bb4601eb9aace9c9e991bf3549a6e1ac6e57b1d (patch) | |
tree | f78f12ceafa786f954aff0ff5407f7208e123bee | |
parent | c43330157961612a211e16d4381ae536d15370fa (diff) | |
download | dotfiles-8bb4601eb9aace9c9e991bf3549a6e1ac6e57b1d.tar.gz dotfiles-8bb4601eb9aace9c9e991bf3549a6e1ac6e57b1d.tar.bz2 dotfiles-8bb4601eb9aace9c9e991bf3549a6e1ac6e57b1d.zip |
enhance isabelle-repair
Diffstat (limited to '')
-rw-r--r-- | .emacs | 39 | ||||
-rw-r--r-- | .emacs.d/evil-settings.el | 2 |
2 files changed, 24 insertions, 17 deletions
@@ -29,22 +29,29 @@ ;; 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) +;; work around bugs in Isabelle/PG +;; we need to toggle options twice to make them work +(defun isabelle-repair (what part) + (let* + ((msg (format "Repairing Auto %s" (capitalize what))) + ; create the variable from `what` and `part` + ; replace spaces by "-" in `what` + (var (format "isar-%s:auto-%s" part + (mapconcat 'identity (split-string (downcase what)) "-"))) + (vart (concat var "-toggle")) + (repair `(lambda () + ; intern-soft also handles the case, that `var` is not existing + ; (it returns nil then -- making `when` skip) + (when (intern-soft ,var) + (message ,msg) + (funcall (intern ,vart) 0) ; toggle off + (funcall (intern ,vart) 1) ; toggle on + )))) + + (add-hook 'proof-shell-init-hook repair))) + +(isabelle-repair "solve direct" "tracing") +(isabelle-repair "quickcheck" "tracing") ;; custom file (setq custom-file "~/.emacs.d/custom.el") diff --git a/.emacs.d/evil-settings.el b/.emacs.d/evil-settings.el index 90d0396..9821a4f 100644 --- a/.emacs.d/evil-settings.el +++ b/.emacs.d/evil-settings.el @@ -13,7 +13,7 @@ ; make unicode-tokens work (setq repair-unicode-shortcuts '(progn - (print "Repairing Unicode Shortcuts for Evil") + (message "Repairing Unicode Shortcuts for Evil") (unicode-tokens-use-shortcuts 0) (unicode-tokens-use-shortcuts 1))) |