diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-10-17 11:10:30 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-10-17 11:10:30 +0000 |
| commit | 2218f6c7b27e09623fcb7f94ddd2c5f6291a3bd3 (patch) | |
| tree | dd23868b01e3c0b2969ea6fa17aed7b0e11afd6d /isar | |
| parent | fd9b1212b63785d7938a48b81f8c7700166aedd1 (diff) | |
Add fix and regression test for Trac #138
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-autotest.el | 10 |
1 files changed, 10 insertions, 0 deletions
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") |