diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-24 19:52:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-24 19:52:08 +0000 |
| commit | 5cd9ba766ecda008b9f6fdce89d1898579497b26 (patch) | |
| tree | eae12e087679d99fac56bac88bddbeec83adbe80 /isar | |
| parent | b0e087829c9089a3ba5a64a4fedaf756cf274178 (diff) | |
isar-set-undo-commands: encourage the user not to change while processing a buffer
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el index 91bc652d..e656c874 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -244,6 +244,9 @@ See -k option for Isabelle interface script." :eval (isar-set-proof-find-theorems-command)) (defun isar-set-undo-commands () + (proof-deactivate-scripting) + (when proof-script-buffer + (message "Warning: switching undo mechanism will break undo in this buffer")) (setq proof-count-undos-fn 'isar-count-undos) (when isar-use-linear-undo (setq proof-kill-goal-command nil) @@ -254,7 +257,7 @@ See -k option for Isabelle interface script." (setq proof-find-and-forget-fn 'isar-find-and-forget) (setq proof-arbitrary-undo-positions nil))) -(defpacustom use-linear-undo t +(defpacustom use-linear-undo nil "Whether to allow undo to re-enter completed proofs (requires restart)." :type 'boolean :eval (isar-set-undo-commands)) |