From 2218f6c7b27e09623fcb7f94ddd2c5f6291a3bd3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 17 Oct 2011 11:10:30 +0000 Subject: Add fix and regression test for Trac #138 --- isar/isar-autotest.el | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'isar') diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index f24e3450..a98dc664 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -46,6 +46,7 @@ (proof-shell-wait) (pg-autotest eval (proof-process-buffer)) (pg-autotest assert-full) + ;; Speed up prover (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) @@ -69,6 +70,15 @@ (pg-autotest eval (insert "end")) (proof-electric-terminator) (pg-autotest assert-full) + ;; Test Trac#138 + (pg-autotest eval (proof-undo-last-successful-command)) + (proof-shell-wait) + (pg-autotest eval (proof-goto-end-of-locked)) + (pg-autotest eval (insert "(* this is a comment *)")) + (pg-autotest eval (proof-goto-point)) + (proof-shell-wait) + (pg-autotest eval (skip-chars-backward " \n\t")) + (pg-autotest eval (insert " ")) ;; shouldn't give read-only error! (set-buffer-modified-p nil) (kill-buffer ".autotest.thy") -- cgit v1.2.3