From 8bb4601eb9aace9c9e991bf3549a6e1ac6e57b1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20=27Necoro=27=20Neumann?= Date: Wed, 5 Sep 2012 10:31:13 +0200 Subject: enhance isabelle-repair --- .emacs | 39 +++++++++++++++++++++++---------------- 1 file changed, 23 insertions(+), 16 deletions(-) (limited to '.emacs') diff --git a/.emacs b/.emacs index 7918b26..3e24c15 100644 --- a/.emacs +++ b/.emacs @@ -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") -- cgit v1.2.3