-*- outline -*-

* Summary of Changes for Proof General 3.3 from 3.2

** Generic Changes

*** Visibility control for completed proofs

     You can make proofs invisible using a context sensitive menu
     (right button on a completed proof), or as soon as they are
     completed with the "Options -> Disappearing Proofs" option.
     Two menu items "Show proofs" and "Hide proofs" apply to
     all the completed proofs in the buffer.

     Notes: 
      1. Proofs of theorems with the same name are not 
         distinguished, visibility controlled together.
      2. FSF Emacs implementation is flaky

*** Proof General startup script welcomes user
 
     The "binary" (startup script) bin/proofgeneral now loads
     PG and invokes a function to display a splash message,
     which invites the user to load a file.   A bit more
     friendly than simply being confronted by a standard 
     XEmacs screen.

*** Changes to Proof General RPM packaging mechanism
  
     Can now build RPM packages with "rpm -ta" from tarball source.
     RPM includes menu file and icons (tested under Linux Mandrake).
     We no longer distribute an SRPM.

*** Command to insert last output as comment in proof script.

     Sometimes it is useful to paste some of the output from
     goals or response buffer into the proof script.  A new
     function `pg-insert-last-output-as-comment' (C-c C-;)
     inserts the last output and converts it into a comment
     using `comment-region'.

*** Compatibility fixes.

     Fixes for FSF Emacs and XEmacs 21.4

     Better support for win32 versions of XEmacs (see README.windows).

     Fixes for recent version 3.3g of X-Symbol (and note on
      web page about using ~/.xemacs/xemacs-packages/ for install locn).

*** Bug fixes.

     XEmacs 21.1 has faulty implementation of buffer-syntactic-context,
     workaround added.  (Symptom was parsing breaking, giving unexpected
     "I can't see any complete commands to process!" error message, esp
     with strings broken across lines containing parentheses).

     Fixed Emacs-confusion minibuffer contents switching bug.  (Bug 
     was triggered by using toolbar while minibuffer active).

** Coq Changes

     Compatibility for V7 added.

     Experimental enhancements to handling of compiled files and 
     file dependency.  (Only tested with Coq 6.3.1: we need help
     from Coq implementors to add primitive support in V7, please
     appeal to them to help Proof General!).

       1) At the end of scripting foo.v (i.e. when activing scripting is
       switched off), "Reset Initial. Compile Module <foo>" is
       automatically issued. This clears the context and writes a .vo file,
       to keep your .vo files up to date. It means that when using PG Coq, 
       you should use the correct commands ("Require foo.") to load all
       the modules you depend on, so that scripting can continue in the
       next file.

       2) PG tracks file dependencies by noticing "Reinterning" messages
       from Coq.  When a file "b.v" is processed which has a "Require a", 
       command, PG will try to find "a.v" and will automatically lock
       it.  (This part of the process is fragile, for two reasons: it
       is hard to find the directory for a.v, since Coq doesn't report
       it, and the reinterning message is only issued the first time the
       file is reinterned).

       3) When a file is retracted, PG attempts to automatically unlock
       all the dependent files, by issuing a coqdep command to determine
       the dependencies.  (This is a rather nasty hack, it's hoped for
       the future that Coq will support this functionality directly).

     This functionality is enabled with the Coq settings option 
     "Auto Compile Vos".


** Isabelle Changes

   Support for theorem dependency tracking: context-sensitive menu  
   (right button on a completed proof) provides a facility for browsing 
   the ancestors and child theorems of a theorem, and highlighting them.  

   The idea of this feature is that it can help you untangle and
   rearrange big proof scripts, by seeing which parts are
   interdependent.
 
   This facility is not yet closely integrated with Isabelle and
   relies on an auxiliary ML file which is only compatible with
   Isabelle99-2.  It is only supplied for Isabelle/classic.

   To activate the feature, use the Isabelle setting option "Theorem
   Dependencies."  Notice that you need to switch this on *after*
   starting an Isabelles session, and must switch on/off on every
   restart.  (This behaviour will improve once better integrated 
   with Isabelle).

   Not yet documented.    Comments and suggestions welcome.


** Changes for developers to note

*** proof-shell-process-output now sets proof-shell-last-output and
    proof-shell-last-output-kind which gives clearer interface internally
    and with rest of code.   See docs.

*** Support for "tracing" buffers added.   
    This was added for Isabelle's simplifier tracing, when a large
    amount of output is produced during a proof for debugging.
    The user would rather see the output as it arrives than wait
    for a long time. 
    Experimental stage and not yet enabled for any prover.  
    See proof-shell-spill-output-regexp.