summaryrefslogtreecommitdiff
path: root/.emacs
diff options
context:
space:
mode:
Diffstat (limited to '.emacs')
-rw-r--r--.emacs17
1 files changed, 17 insertions, 0 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)