Some test cases for Proof General.
==================================

8.12.98  INHIBIT VARIABLES
==========================

  Test with proof-splash-inhibit=t

  Test with proof-toolbar-inhibit=t
  

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

11.12.98  RUDELY KILLING THE ACTIVE SCRIPTING BUFFER
====================================================

  Start scripting with some buffer, after
  having processed another buffer.

  Kill it when scripting is only partly finished.

  Scripting should be cleanly turned off and it
  should be possible to resume retraction in the 
  first buffer.

  Moreover, this ensures that if the file is on the included
  files list, yet has been only partly processed (e.g. because
  Undo steps were taken), then it will be retracted and
  removed from the included files list.

  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 

    M-x proof-shell-exit

  Process should exit cleanly.