[isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)



Hi,

(some of) the options set for Isabelle in ProofGeneral (like "Auto Solve
Direct", "Auto Quickcheck") are not active, even though they are
enabled. I don't know whether this bug lives in PG or in Isabelle...

Anyways: A normal workaround is to disable and enable these options
again in the menu -- which is cumbersome.

Hence: Find attached an Elisp-function 'isabelle-repair', which does
this toggling for you after Isabelle startup. Perhaps somebody finds
this useful :)

This function can then be called for each parameter that matters for you:

(isabelle-repair "auto solve direct" "tracing")
(isabelle-repair "auto quickcheck" "tracing")

Probably, this could be expanded to repair every option that has the
problem, but I don't know on how to collect them.

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055
;; 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 %s" (capitalize what)))
     ; create the variable from `what` and `part`
     ; replace spaces by "-" in `what`
     (var (format "isar-%s:%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)))



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.