From c43eebc79e84402f3978f1f32d812e755039e3ef Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 13 Feb 2005 21:36:23 +0000
Subject: Added simple testing framework (in progress)

---
 isar/isar-autotest.el | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 isar/isar-autotest.el

(limited to 'isar')

diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
new file mode 100644
index 00000000..5cd5b2b8
--- /dev/null
+++ b/isar/isar-autotest.el
@@ -0,0 +1,35 @@
+;; isar-autotest.el: tests of Isar Proof General.
+;;
+;; You can run these by issuing "make devel.test.isar" in PG home dir.
+;;
+;; $Id$
+;;
+
+(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")
+
+; These require Complex theory
+;(pg-autotest script-wholefile "isar/Root2_Isar.thy")
+;(pg-autotest script-wholefile "isar/Root2_Tactic.thy")
+
+;; 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)
+
+
-- 
cgit v1.2.3