From ebe2ce9e1cc8475e4fdf79e6c7a548315a7fa3e7 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 21 Jan 1999 14:20:35 +0000 Subject: Rearranged into reverse chronological order --- etc/TESTS | 60 +++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 33 insertions(+), 27 deletions(-) diff --git a/etc/TESTS b/etc/TESTS index 2299965b..08800069 100644 --- a/etc/TESTS +++ b/etc/TESTS @@ -1,30 +1,26 @@ Some test cases for Proof General. ================================== -8.12.98 INHIBIT VARIABLES -========================== +See testing-log.txt for log of tests conducted. +Please add to that file! - Test with proof-splash-inhibit=t - Test with proof-toolbar-inhibit=t - +15.1.99 LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS +=================================================== -8.12.98 SCRIPTING FOR BUFFERS WITHOUT FILES. -============================================= + Test that etc/isa/long-line-backslash.ML can be processed + successfully. - Switch to a fresh buffer FOO which doesn't visit a file. - Do M-x isa-mode RET. - Should succeed. - Try asserting commands, e.g. Goal "P-->P"; - Switch to another fresh buffer BAR, turn on isa-mode. - Should succeed again. - Try asserting commands here, e.g. Goal "Q&Q --> Q"; - Should give error "Cannot have more than one active scripting buffer". +16.12.98 KILLING THE PROOF PROCESS +================================== - Exit emacs. Should query whether we want to save these - scripting buffers (maybe XEmacs only). + Process some proof script buffer. Invoke + + M-x proof-shell-exit + Process should exit cleanly. + 11.12.98 RUDELY KILLING THE ACTIVE SCRIPTING BUFFER ==================================================== @@ -45,20 +41,30 @@ Some test cases for Proof General. FIXME: Using C-x C-v to revert to saved version doesn't seem to work because it renames the buffer or something. -16.12.98 KILLING THE PROOF PROCESS -================================== - - Process some proof script buffer. Invoke +8.12.98 INHIBIT VARIABLES +========================== - M-x proof-shell-exit + Test with proof-splash-inhibit=t - Process should exit cleanly. + Test with proof-toolbar-inhibit=t -15.1.99 LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS -=================================================== - Test that etc/isa/long-line-backslash.ML can be processed - successfully. +8.12.98 SCRIPTING FOR BUFFERS WITHOUT FILES. +============================================= + + Switch to a fresh buffer FOO which doesn't visit a file. + Do M-x isa-mode RET. + Should succeed. + Try asserting commands, e.g. Goal "P-->P"; + + Switch to another fresh buffer BAR, turn on isa-mode. + Should succeed again. + Try asserting commands here, e.g. Goal "Q&Q --> Q"; + Should give error "Cannot have more than one active scripting buffer". + + Exit emacs. Should query whether we want to save these + scripting buffers (maybe XEmacs only). + -- cgit v1.2.3