diff options
| author | David Aspinall | 2007-12-14 01:22:59 +0000 |
|---|---|---|
| committer | David Aspinall | 2007-12-14 01:22:59 +0000 |
| commit | 1f8b780b72b36b9ca4605453b9fe73bbc9dd4c23 (patch) | |
| tree | 9bae546af0e8a4804246121c99525b2b81ea315d /isar | |
| parent | 8fa863dea38eb6471bc99f05328b53430fd78f8d (diff) | |
Improve loading; these tests are not functioning yet
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-autotest.el | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index b20dc1ae..2d5beef5 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -7,10 +7,12 @@ (require 'pg-autotest) -;; The included test files -(pg-autotest message "Testing standard Example.thy, Example-Xsym.thy") -(pg-autotest script-wholefile "isar/Example.thy") -(pg-autotest script-wholefile "isar/Example-Xsym.thy") +(eval-when (load) + + ;; The included test files + (pg-autotest message "Testing standard Example.thy, Example-Xsym.thy") + (pg-autotest script-wholefile "isar/Example.thy") + (pg-autotest script-wholefile "isar/Example-Xsym.thy") ; These require Complex theory ;(pg-autotest script-wholefile "isar/Root2_Isar.thy") @@ -18,18 +20,18 @@ ;; The standard simple multiple file examples -(pg-autotest message "Simple test of multiple files...") -(pg-autotest script-wholefile "etc/isar/multiple/C.thy") -(pg-autotest assert-processed "etc/isar/multiple/C.thy") -(pg-autotest assert-processed "etc/isar/multiple/A.thy") -(pg-autotest assert-processed "etc/isar/multiple/B.thy") -(pg-autotest retract-file "etc/isar/multiple/B.thy") -(pg-autotest assert-unprocessed "etc/isar/multiple/B.thy") -(pg-autotest assert-unprocessed "etc/isar/multiple/C.thy") -(pg-autotest assert-processed "etc/isar/multiple/A.thy") - - -(pg-autotest-quit-prover) -(pg-autotest-finished) + (pg-autotest message "Simple test of multiple files...") + (pg-autotest script-wholefile "etc/isar/multiple/C.thy") + (pg-autotest assert-processed "etc/isar/multiple/C.thy") + (pg-autotest assert-processed "etc/isar/multiple/A.thy") + (pg-autotest assert-processed "etc/isar/multiple/B.thy") + (pg-autotest retract-file "etc/isar/multiple/B.thy") + (pg-autotest assert-unprocessed "etc/isar/multiple/B.thy") + (pg-autotest assert-unprocessed "etc/isar/multiple/C.thy") + (pg-autotest assert-processed "etc/isar/multiple/A.thy") + + + (pg-autotest-quit-prover) + (pg-autotest-finished)) |