;; isar-autotest.el: tests of Isar Proof General.
;;
;; You can run these by issuing "make test.isar" in PG home dir.
;;
;; isar-autotest.el,v 9.0 2008/01/30 15:22:19 da Exp
;;

(require 'pg-autotest)

(unless noninteractive

  ;; 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))


