enhance isabelle-repair

1 files changed, 23 insertions, 16 deletions

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")