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

See testing-log.txt for log of tests conducted.
Please add to that file!


22.3.00 FILENAME ESCAPES PROBLEM [All provers, probably]
========================================================

  Filename substitution %s in settings including proof-shell-cd-cmd,
  proof-shell-inform-file-{retracted,processed}-cmd, may need
  to add escape characters peculiar to the proof assistant syntax.

  Test cases:

     ln -s ProofGeneral \\backslash  
     ln -s ProofGeneral \"quote

  Then try scripting with example files for each prover,
  i.e.  \"quote/coq/example.v, etc.


1.2.99 FILE RECOGNITION PROBLEM  [Isabelle]
===========================================

  Bug in regexp caused ML files to be recognized as
  theory files when "thy" appeared in path.
  Test case in etc/isa/thy/test.ML.


15.1.99  LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS
===================================================

  Test that etc/isa/long-line-backslash.ML can be processed
  successfully.


16.12.98 KILLING THE PROOF PROCESS
==================================

  Process some proof script buffer. Invoke 

    M-x proof-shell-exit

  Process should exit cleanly.
  
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.

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