From 4ccf993e70f3755c01add46076e66ca40b740ad8 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 27 Aug 2010 23:01:22 +0000 Subject: Fix bug with nested spans, solving #344/#335 --- isar/isar-autotest.el | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'isar/isar-autotest.el') diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index cdf69a1b..18c0db81 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -33,6 +33,21 @@ (pg-autotest remark "Testing standard Example.thy, Example-Xsym.thy") (pg-autotest script-wholefile "isar/Example.thy") + ;; Test Trac#344 (nested spans bug with old-style undo) + ;; TODO: should test with both undo styles + (pg-autotest eval (proof-retract-buffer)) + (proof-shell-wait) + (goto-char 135) ; first line + (pg-autotest eval (proof-goto-point)) + (proof-shell-wait) + (pg-autotest eval (proof-retract-buffer)) + (proof-shell-wait) + (goto-char 135) ; first line + (pg-autotest eval (proof-goto-point)) + (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)) (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! @@ -63,7 +78,7 @@ (pg-autotest script-wholefile "isar/Example-Tokens.thy") (pg-autotest remark "Testing random jumps and edits") - (pg-autotest script-randomjumps "isar/Example.thy" 5) + (pg-autotest script-randomjumps "isar/Example.thy" 8) (when isar-long-tests (pg-autotest remark "Larger files...") -- cgit v1.2.3