diff options
Diffstat (limited to 'generic/pg-autotest.el')
| -rw-r--r-- | generic/pg-autotest.el | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index 8dfee09d..e7cb19a9 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -1,10 +1,18 @@ ;;; pg-autotest.el --- Simple testing framework for Proof General -;; -;; Copyright (C) 2005, 2009-11 LFCS Edinburgh, David Aspinall. + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall -;; + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; + ;;; Commentary: ;; ;; Support for running a series of scripted UI tests. @@ -14,8 +22,8 @@ ;; -- add macros for defining test suites ;; -- add more precise functional tests to check results ;; -- add negative tests -;; -;; $Id$ + +;;; Code: (require 'proof-splash) (setq proof-splash-enable nil) ; prevent splash when testing @@ -96,7 +104,7 @@ (format-time-string "%D %H:%M"))))) (defun pg-autotest-message (msg &rest args) - "Give message MSG in log file output and on display." + "Give message MSG (formatted using ARGS) in log file output and on display." (let ((fmsg (if args (apply 'format msg args) msg))) (proof-with-current-buffer-if-exists pg-autotest-log @@ -209,7 +217,7 @@ completely processing the buffer as the last step." (proof-shell-wait) (decf jumps)) - ((and (eq random-thing 1) + ((and (eq random-thing 1) (not (proof-locked-region-empty-p))) (pg-autotest-message " random jump: retracting whole buffer") @@ -272,7 +280,7 @@ completely processing the buffer as the last step." (defun pg-autotest-test-quit-prover () "Exit prover process." (if (buffer-live-p proof-shell-buffer) - (let ((kill-buffer-query-functions nil)) + (let ((kill-buffer-query-functions nil)) (kill-buffer proof-shell-buffer)) (error "No proof shell buffer to kill"))) |