From f4abdf67e0996455b8ccbd1baa68bf64691d9c11 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 11 Oct 2010 00:26:42 +0000 Subject: isar-set-undo-commands: prevent opening new script files calling proof-deactivate-scripting --- isar/isar.el | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'isar') diff --git a/isar/isar.el b/isar/isar.el index feea1f4d..b32c0825 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -243,10 +243,11 @@ See -k option for Isabelle interface script." :type 'boolean :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")) +(defun isar-set-undo-commands (&optional initp) + (unless initp + (proof-deactivate-scripting) + (when proof-script-buffer + (message "Warning: switching undo mechanism will break undo in current buffer"))) (setq proof-count-undos-fn 'isar-count-undos) (when isar-use-linear-undo (setq proof-kill-goal-command nil) @@ -264,7 +265,7 @@ See -k option for Isabelle interface script." (defun isar-configure-from-settings () (isar-set-proof-find-theorems-command) - (isar-set-undo-commands)) + (isar-set-undo-commands 'init)) ;; ;; Theory loader operations -- cgit v1.2.3