PG-adapting.texi

\input texinfo
@c TODO: setting for configuring proof hidden regions.
@c
@c $Id$
@c
@c NB: the first line of this file uses a non-standard TeXinfo
@c hack to print in Serifa fonts.  It has no effect if you don't have
@c my hacked version of TeXinfo - da.
@c
@c 
@setfilename PG-adapting.info
@settitle Adapting Proof General
@setchapternewpage odd
@paragraphindent 0
@iftex
@afourpaper
@end iftex

@c
@c Some URLs.
@c FIXME: unfortunately, broken in buggy pdftexinfo.
@c so removed for now.
@set URLisamode  http://homepages.inf.ed.ac.uk/da/isamode
@set URLpghome   https://proofgeneral.github.io
@set URLpglatestrpm  http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest.noarch.rpm
@set URLpglatesttar  http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest.tar.gz
@set URLpglatestdev  http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-devel-latest.tar.gz
@c
@c

@c
@c IMPORTANT NOTE ABOUT THIS TEXINFO FILE:
@c I've tried keep full node lines *out* of this file because Emacs makes a
@c mess of updating them and they are a nuisance to do by hand.  
@c Instead, rely on makeinfo and friends to do the equivalent job.  
@c For this to work, we must follow each node
@c immediately with a section command, i.e.:
@c
@c  @node node-name
@c  <section-command>
@c
@c And each section with lower levels must have a menu command in
@c it.  Menu updating with Emacs is a bit better than node updating,
@c but tends to delete the first section of the file in XEmacs!
@c (it's better in GNU Emacs at the time of writing).
@c
@c
@c reminder about references: 
@c        @xref{node}  blah         start of sentence: See [ref]
@c        blah (@pxref{node}) blah  bla (see [ref]), best at end of sentence
@c        @ref{node}                without "see". Careful for info.


@set version 4.6-git
@set emacsversion 25.2
@set last-update July 2022
@set rcsid $Id$

@dircategory Theorem proving
@direntry
* Adapting PG: (PG-adapting). Adapt Proof General to new provers
END-INFO-DIR-ENTRY
@end direntry

@c
@c MACROS
@c
@c define one here for a command with a key-binding?
@c
@c I like the idea, but it's maybe against the TeXinfo
@c style to fix together a command and its key-binding.
@c
@c merge functions and variables into concept index.
@c @syncodeindex fn cp
@c @syncodeindex vr cp

@c merge functions into variables index
@c @syncodeindex fn vr

@finalout
@titlepage
@title Adapting Proof General
@subtitle Proof General --- Organize your proofs!
@sp 1
@subtitle Adapting Proof General @value{version} to new provers
@subtitle @value{last-update}
@subtitle @b{proofgeneral.github.io}

@iftex
@vskip 1cm
@image{ProofGeneral-image}
@end iftex
@author David Aspinall with T. Kleymann
@page
@vskip 0pt plus 1filll
This manual and the program Proof General are
Copyright @copyright{} 2000-2011 by members
of the Proof General team, LFCS Edinburgh.


@c
@c COPYING NOTICE
@c
@ignore
Permission is granted to process this file through TeX and print the
results, provided the printed document carries copying permission notice
identical to this one except for the removal of this paragraph (this
paragraph not being relevant to the printed manual).
@end ignore

@sp 2
Permission is granted to make and distribute verbatim copies of this
manual provided the copyright notice and this permission notice are
preserved on all copies.  
@sp 2

This manual documents Proof General, Version @value{version}, for use
GNU Emacs @value{emacsversion} or (as far as possible) later versions.
Proof General is distributed under the terms of the GNU General Public
License (GPL), version 3 or later;
please check the accompanying file @file{COPYING} for more details.

@sp 1

Visit Proof General on the web at @code{https://proofgeneral.github.io}

@c (commented; dates from CVS) Version control: @code{@value{rcsid}}
@end titlepage

@page


@ifinfo
@node Top
@top Proof General

This file documents configuration mechanisms for version @value{version}
of @b{Proof General}, a generic Emacs interface for proof assistants.

Proof General @value{version} has been tested with GNU Emacs
@value{emacsversion}.  It is supplied ready customized for the proof
assistants Coq, EasyCrypt, qrhl-tool, and PhoX.

This manual contains information for customizing to new proof
assistants; see the user manual for details about how to use
Proof General.

@menu
* Introduction::
* Beginning with a New Prover::
* Menus and Toolbar and User-level Commands::  
* Proof Script Settings::       
* Proof Shell Settings::        
* Goals Buffer Settings::  
* Splash Screen Settings::      
* Global Constants::            
* Handling Multiple Files::     
* Configuring Editing Syntax::
* Configuring Font Lock::
* Configuring Tokens::
* Configuring Proof-Tree Visualization::
* Writing More Lisp Code::
* Internals of Proof General::  
* Plans and Ideas::             
* Demonstration Instantiations::
* Function Index::              
* Variable Index::              
* Concept Index::               
@end menu
@end ifinfo

@node Introduction
@unnumbered Introduction

Welcome to Proof General!

Proof General a generic Emacs-based interface for proof assistants.

This manual contains information for adapting Proof General to new proof
assistants, and some sketches of the internal implementation.  It is not
intended for most ordinary users of the system.  
For full details about how to use Proof General, and information on its
availability and installation, please see the main Proof General manual
which should accompany this one.

We positively encourage the support of new systems.  Proof General has
grown more flexible and useful as it has been adapted to more proof
assistants.  

Typically, adding support for a new prover improves support for others,
both because the code becomes more robust, and because new ideas are
brought into the generic setting.  Notice that the Proof General
framework has been built as a "product line architecture": generality
has been introduced step-by-step in a demand-driven way, rather than at
the outset as a grand design.  Despite this strategy, the interface has
a surprisingly clean structure.  The approach means that we fully expect
hiccups when adding support for new assistants, so the generic core may
need extension or modification.  To support this we have an open
development method: if you require changes in the generic support,
please contact us (or make adjustments yourself and send them to us).

Proof General has a home page at
@uref{https://proofgeneral.github.io}.  Visit this page
for the latest version of the manuals, other documentation, system
downloads, etc.


@menu
* Future::
* Credits::
@end menu

@node Future
@unnumberedsec Future
@cindex Proof General Kit
@cindex Future

The aim of the Proof General project is to provide a powerful and
configurable interfaces which help user-interaction with interactive
proof assistants.  

The strategy Proof General uses is to targets power users rather than
novices; other interfaces have often neglected this class of users.  But
we do include general user interface niceties, such as toolbar and
menus, which make use easier for all.

Proof General has been Emacs based so far, but plans are afoot to
liberate it from the points and parentheses of Emacs Lisp.  The
successor project Proof General Kit proposes that proof assistants use a
@i{standard} XML-based protocol for interactive proof, dubbed @b{PGIP}.

PGIP enables middleware for interactive proof tools and interface
components.  Rather than configuring Proof General for your proof
assistant, you will need to configure your proof assistant to understand
PGIP.  There is a similarity however; the design of PGIP was based
heavily on the Emacs Proof General framework.  This means that effort on
customizing Emacs Proof General to a new proof assistant is worthwhile
even in the light of PGIP: it will help you to understand Proof
General's model of interaction, and moreover, we hope to use the Emacs
customizations to provide experimental filters which allow supported
provers to communicate using PGIP.

At the time of writing, these ideas are in early stages. For latest
details, or to become involved, see
@uref{http://proofgeneral.inf.ed.ac.uk/kit, the Proof General Kit
webpage}.


@node Credits
@unnumberedsec Credits

David Aspinall put together and wrote most of this manual.  Thomas
Kleymann wrote some of the text in Chapter 8.  Much of the content is
generated automatically from Emacs docstrings, some of which have been
written by other Proof General developers.



@node Beginning with a New Prover
@chapter Beginning with a New Prover

Proof General has about 100 configuration variables which are set on a
per-prover basis to configure the various features.  It may sound like a
lot but don't worry!  Many of the variables occur in pairs (typically
regular expressions matching the start and end of some text), and you
can begin by setting just a fraction of the variables to get the basic
features of script management working.  The bare minimum for a working
prototype is about 25 simple settings.

For more advanced features you may need (or want) to write some Emacs
Lisp.  If you're adding new functionality please consider making it
generic for different proof assistants, if appropriate.  When writing
your modes, please follow the Emacs Lisp conventions, @pxref{Tips,,,Elisp}.

The configuration variables are declared in the file
@file{generic/proof-config.el}.  The details in the central part of this
manual are based on the contents of that file, beginning in @ref{Menus and Toolbar
and User-level Commands}, and continuing until @ref{Global Constants}.
Other chapters cover the details of configuring for multiple files and
for supporting the other Emacs packages mentioned in the user manual
(@i{Support for other Packages}).  If you write additional Elisp code
interfacing to Proof General, you can find out about some useful functions
by reading @ref{Writing More Lisp Code}.  The last chapter of this
manual describes some of the internals of Proof General, in case you are
interested, maybe because you need to extend the generic core to do
something new.

In the rest of this chapter we describe the general mechanisms for
instantiating Proof General.  We assume some knowledge of the content
of the main Proof General manual.

@menu
* Overview of adding a new prover::            
* Demonstration instance and easy configuration::
* Major modes used by Proof General::  
@end menu


@node Overview of adding a new prover
@section Overview of adding a new prover

Each proof assistant supported has its own subdirectory under
@code{proof-home-directory}, used to store a root elisp file and any
other files needed to adapt the proof assistant for Proof General.

@c Here we show how a minimal configuration of Proof General works for
@c Isabelle, without any special changes to Isabelle.

Here is how to go about adding support for a new prover.

@enumerate
@item Make a directory called @file{myassistant/} under the Proof General home
directory @code{proof-home-directory}, to put the specific customization
and associated files in.
@item Add a file @file{myassistant.el} to the new directory.
@item Edit @file{proof-site.el} to add a new entry to the
  @code{proof-assistants-table} variable.  The new entry should look
like this:
@lisp
    (myassistant "My Proof Assistant" "\\.myasst$")
@end lisp    
The first item is used to form the name of the internal variables for
the new mode as well as the directory and file where it loads from.  The
second is a string, naming the proof assistant.  The third item is a
regular expression to match names of proof script files for this
assistant.  See the documentation of @code{proof-assistant-table} for
more details.
@item Define the new Proof General modes in @file{myassistant.el}, 
 by setting configuration variables to customize the
 behaviour of the generic modes.  
@end enumerate

@c You could begin by setting a minimum number of the variables, then
@c adjust the settings via the customize menus, under Proof-General ->
@c Internals.

@c TEXI DOCSTRING MAGIC: proof-assistant-table
@defvar proof-assistant-table 
Proof General's table of supported proof assistants.@*
This is copied from @samp{@code{proof-assistant-table-default}} at load time,
removing any entries that do not have a corresponding directory
under @samp{@code{proof-home-directory}}.

Each entry is a list of the form
@lisp
  (@var{symbol} @var{name} @var{file-extension} [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST])
@end lisp
The @var{name} is a string, naming the proof assistant.
The @var{symbol} is used to form the name of the mode for the
assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp}
(or with extension @var{file-extension}) are visited.  If present,
@var{ignored-extensions-list} is a list of file-name extensions to be
ignored when doing file-name completion (@var{ignored-extensions-list}
is added to @samp{@code{completion-ignored-extensions}}).

@var{symbol} is also used to form the name of the directory and elisp
file for the mode, which will be
@lisp
    @var{proof-home-directory}/@var{symbol}/@var{symbol}.el
@end lisp
where @var{proof-home-directory} is the value of the
variable @samp{@code{proof-home-directory}}.
@end defvar


The final step of the description above is where the work lies.  There
are two basic methods.  You can write some Emacs lisp functions and
define the modes using the macro @code{define-derived-mode}.  Or you can
use the new easy configuration mechanism of Proof General 3.0 described
in the next section, which calls @code{define-derived-mode} for you.
You still need to know which configuration variables should be set, and
how to set them.  

The documentation below (and inside Emacs) should help with that, but
the best way to begin might be to use an existing Proof General instance
as an example.  


@node Demonstration instance and easy configuration
@section Demonstration instance and easy configuration

Proof General is supplied with a demonstration instance for Isabelle
which configures the basic features.  This is a whittled down version of
Isabelle Proof General, which you can use as a template to get support
for a new assistant going.  Check the directory @file{demoisa} for the
two files @file{demoisa.el} and @file{demoisa-easy.el}.

The file @file{demoisa.el} follows the scheme described in @ref{Major
modes used by Proof General}.  It uses the Emacs Lisp macro
@code{define-derived-mode} to define the four modes for a Proof General
instance, by inheriting from the generic code.  Settings which configure
Proof General are made by functions called from within each mode, as
appropriate.

The file @file{demoisa-easy.el} uses a new simplified mechanism to
achieve (virtually) the same result.  It uses the macro
@code{proof-easy-config} defined in @file{proof-easy-configl.el} to make
all of the settings for the Proof General instance in one go, defining
the derived modes automatically using a regular naming scheme.  No lisp
code is used in this file except the call to this macro.  The minor
difference in the end result is that all the variables are set at once,
rather than inside each mode.  But since the configuration variables are
all global variables anyway, this makes no real difference.

The macro @code{proof-easy-config} is called like this:
@lisp
   (proof-easy-config @var{myprover} "@var{MyProver}"
        @var{config_1} @var{val_1}
        ...
        @var{config_n} @var{val_n})
@end lisp
The main body of the macro call is like the body of a @code{setq}.  It
contains pairs of variables and value settings.  The first argument to
the macro is a symbol defining the mode root, the second argument is a
string defining the mode name.  These should be the same as the first
part of the entry in @code{proof-assistant-table} for your prover.
@xref{Overview of adding a new prover}.  After the call to
@code{proof-easy-config}, the new modes @code{@var{myprover}-mode},
@code{@var{myprover}-shell-mode}, @code{@var{myprover}-response-mode},
and @code{@var{myprover}-goals-mode} will be defined.  The configuration
variables in the body will be set immediately.


This mechanism is in fact recommended for new instantiations of
Proof General since it follows a regular pattern, and we can more
easily adapt it in the future to new versions of Proof General.

Even Emacs Lisp experts should prefer the simplified mechanism.  If you
want to set some buffer-local variables in your Proof General modes, or
invoke supporting lisp code, this can easily be done by adding functions
to the appropriate mode hooks after the @code{proof-easy-config} call.
For example, to add extra settings for the shell mode for
@code{demoisa}, we could do this:
@lisp
   (defun demoisa-shell-extra-config ()
      @var{extra configuration ...}
    )
   (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config)
@end lisp
The function to do extra configuration @code{demoisa-shell-extra-config}
is then called as the final step when @code{demoisa-shell-mode} is
entered (be wary, this will be after the generic
@code{proof-shell-config-done} is called, so it will be too late to set
normal configuration variables which may be examined by
@code{proof-shell-config-done}).


@node Major modes used by Proof General
@section Major modes used by Proof General

There are four major modes used by Proof General, one for each type of
buffer it handles.  The buffer types are: script, shell, response and
goals.  Each of these has a generic mode, respectively:
@code{proof-mode}, @code{proof-shell-mode}, @code{proof-response-mode},
and @code{proof-goals-mode}.

The pattern for defining the major mode for an instance of Proof General
is to use @code{define-derived-mode} to define a specific mode to inherit from
each generic one, like this:
@lisp
(define-derived-mode myass-shell-mode proof-shell-mode
   "MyAss shell" nil
   (myass-shell-config)
   (proof-shell-config-done))
@end lisp
Where @code{myass-shell-config} is a function which sets the
configuration variables for the shell (@pxref{Proof Shell Settings}).

It's important that each of your modes invokes one of the functions
 @code{proof-config-done},
 @code{proof-shell-config-done}, 
 @code{proof-response-config-done}, or
 @code{proof-goals-config-done}
once it has set its configuration variables.  These functions
finalize the configuration of the mode.

The modes must be named standardly, replacing @code{proof-} with the
prover's symbol name, @code{@var{PA}-}.  In other words, you must define
@code{@var{PA}-mode}, @code{@var{PA}-shell-mode}, etc.

See the file @file{demoisa.el} for an example of the four calls to
@code{define-derived-mode}.

Aside: notice that the modes are selected using stub functions
inside @code{proof-site.el}, which set the variables
@code{proof-mode-for-script}, @code{proof-mode-for-shell}, etc,
that actually select the right mode.  These variables
are declared in @code{pg-vars.el}.


@node Menus and Toolbar and User-level Commands
@chapter Menus, toolbar, and user-level commands

The variables described in this chapter configure the menus, toolbar,
and user-level commands.  They should be set in the script mode
before @code{proof-config-done} is called.  (Toolbar configuration must
be made before @file{proof-toolbar.el} is loaded, which usually is
triggered automatically by an attempt to display the toolbar).

@menu
* Settings for generic user-level commands::
* Menu configuration::
* Toolbar configuration::
@end menu

@node Settings for generic user-level commands
@section Settings for generic user-level commands

@c TEXI DOCSTRING MAGIC: proof-assistant-home-page
@defvar proof-assistant-home-page 
Web address for information on proof assistant.@*
Used for Proof General's help menu.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-context-command
@defvar proof-context-command 
Command to display the context in proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-info-command
@defvar proof-info-command 
Command to ask for help or information in the proof assistant.@*
String or fn.  If a string, the command to use.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-showproof-command
@defvar proof-showproof-command 
Command to display proof state in proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goal-command
@defvar proof-goal-command 
Command to set a goal in the proof assistant.  String or fn.@*
If a string, the format character @samp{%s} will be replaced by the
goal string.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-save-command
@defvar proof-save-command 
Command to save a proved theorem in the proof assistant.  String or fn.@*
If a string, the format character @samp{%s} will be replaced by the
theorem name.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-find-theorems-command
@defvar proof-find-theorems-command 
Command to search for a theorem containing a given term.  String or fn.@*
If a string, the format character @samp{%s} will be replaced by the term.
If a function, it should return the command string to send.
@end defvar



@node Menu configuration
@section Menu configuration

As well as the generic Proof General menu, each proof assistant is
provided with a specific menu which can have prover-specific commands.
Proof General puts some default things on this menu, including the
commands to start/stop the prover, and the user-extensible "Favourites"
menu.

@c TEXI DOCSTRING MAGIC: PA-menu-entries
@defvar PA-menu-entries 
Extra entries for proof assistant specific menu.@*
A list of menu items [@var{name} @var{callback} @var{enabler} ...].  See the documentation
of @samp{@code{easy-menu-define}} for more details.
@end defvar

@c TEXI DOCSTRING MAGIC: PA-help-menu-entries
@defvar PA-help-menu-entries 
Extra entries for help submenu for proof assistant specific help menu.@*
A list of menu items [@var{name} @var{callback} @var{enabler} ...].  See the documentation
of @samp{@code{easy-menu-define}} for more details.
@end defvar


@node Toolbar configuration
@section Toolbar configuration

Unlike the menus, Proof General has only one toolbar.  For the "generic"
aspect of Proof General to work well, we shouldn't change (the meaning
of) the existing toolbar buttons too far.  This would discourage people
from experimenting with different proof assistants when they don't
really know them, which is one of the advantages that Proof General
brings.

But in case it is hard to map some of the generic buttons
onto functions in particular provers, and to allow extra
buttons, there is a mechanism for adjustment.

I used The Gimp to create the buttons for Proof General.  The
development distribution includes a button blank and some notes in
@file{etc/notes.txt} about making new buttons.


@c TEXI DOCSTRING MAGIC: proof-toolbar-entries-default
@defvar proof-toolbar-entries-default 
Example value for proof-toolbar-entries.  Also used to define scripting menu.@*
This gives a bare toolbar that works for any prover, providing the
appropriate configuration variables are set.
To add/remove prover specific buttons, adjust the @samp{<PA>-toolbar-entries}
variable, and follow the pattern in @samp{proof-toolbar.el} for
defining functions, images.
@end defvar

@c TEXI DOCSTRING MAGIC: PA-toolbar-entries
@defvar PA-toolbar-entries 
List of entries for Proof General toolbar and Scripting menu.@*
Format of each entry is (@var{token} @var{menuname} @var{tooltip} @var{toolbar-p} [VISIBLE-P]).

For each @var{token}, we expect an icon with base filename @var{token},
a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler
proof-toolbar-<TOKEN>-enable-p.

If @var{visible-p} is absent, or evaluates to non-nil, the item will
appear on the toolbar or menu.  If it evaluates to nil, the item
is not shown.

If @var{menuname} is nil, item will not appear on the scripting menu.

If @var{toolbar-p} is nil, item will not appear on the toolbar.

The default value is @samp{@code{proof-toolbar-entries-default}} which contains
the standard Proof General buttons.
@end defvar

Here's an example of how to remove a button, from @file{af2.el}:
@lisp
(setq af2-toolbar-entries
      (assq-delete-all 'state af2-toolbar-entries))
@end lisp



@c defgroup proof-script
@node Proof Script Settings
@chapter Proof Script Settings

The variables described in this chapter should be set in the script mode
before @code{proof-config-done} is called.  These variables configure
recognition of commands in the proof script, and also control some of
the behaviour of script management.


@menu
* Recognizing commands and comments::
* Recognizing proofs::
* Recognizing other elements::
* Configuring undo behaviour::
* Nested proofs::
* Omitting proofs for speed::
* Safe (state-preserving) commands::
* Activate scripting hook::
* Automatic multiple files::
* Completely asserted buffers::
* Completions::
@end menu


@node Recognizing commands and comments
@section Recognizing commands and comments

The first four settings configure the generic parsing strategy for
commands in the proof script.  Usually only one of these three needs to
be set.  If the generic parsing functions are not flexible for your
needs, you can supply a value for @code{proof-script-parse-function}.

Note that for the generic functions to work properly, it is
@strong{essential} that you set the syntax table for your mode properly,
so that comments and strings are recognized.  See the Emacs
documentation to discover how to do this (particularly for the function
@code{modify-syntax-entry}, (@pxref{Syntax Tables,,,Elisp}).

@xref{Proof script mode}, for more details of the parsing
functions.

@c TEXI DOCSTRING MAGIC: proof-terminal-string
@defvar proof-terminal-string 
String that terminates commands sent to prover; nil if none.

To configure command recognition properly, you must set at least one
of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}},
@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}},
or @samp{@code{proof-script-parse-function}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-electric-terminator-noterminator
@defvar proof-electric-terminator-noterminator 
If non-nil, electric terminator does not actually insert a terminator.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-script-sexp-commands
@defvar proof-script-sexp-commands 
Non-nil if script has Lisp-like syntax: commands are @code{top-level} sexps.@*
You should set this variable in script mode configuration.

To configure command recognition properly, you must set at least one
of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}},
@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}},
or @samp{@code{proof-script-parse-function}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-command-start-regexp
@defvar proof-script-command-start-regexp 
Regular expression which matches start of commands in proof script.@*
You should set this variable in script mode configuration.

To configure command recognition properly, you must set at least one
of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}},
@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}},
or @samp{@code{proof-script-parse-function}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-command-end-regexp
@defvar proof-script-command-end-regexp 
Regular expression which matches end of commands in proof script.@*
You should set this variable in script mode configuration.

The end of the command is considered to be the end of the match
of this regexp.  The regexp may include a nested group, which
can be used to recognize the start of the following command
(or white space).  If there is a nested group, the end of the
command is considered to be the start of the nested group,
i.e. (@code{match-beginning} 1), rather than (@code{match-end} 0).

To configure command recognition properly, you must set at least one
of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}},
@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}},
or @samp{@code{proof-script-parse-function}}.
@end defvar


The next four settings configure the comment syntax.  Notice that to get
reliable behaviour of the parsing functions, you may need to modify the
syntax table for your prover's mode.  
Read the Elisp manual (@pxref{Syntax Tables,,,Elisp}) for details about that.

@c TEXI DOCSTRING MAGIC: proof-script-comment-start
@defvar proof-script-comment-start 
String which starts a comment in the proof assistant command language.@*
The script buffer's @samp{@code{comment-start}} is set to this string plus a space.
Moreover, comments are usually ignored during script management, and not
sent to the proof process.

You should set this variable for reliable working of Proof General,
as well as @samp{@code{proof-script-comment-end}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-script-comment-start-regexp
@defvar proof-script-comment-start-regexp 
Regexp which matches a comment start in the proof command language.

The default value for this is set as (@code{regexp-quote} @samp{@code{proof-script-comment-start}})
but you can set this variable to something else more precise if necessary.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-comment-end
@defvar proof-script-comment-end 
String which ends a comment in the proof assistant command language.@*
Should be an empty string if comments are terminated by @samp{@code{end-of-line}}
The script buffer's @samp{@code{comment-end}} is set to a space plus this string,
if it is non-empty.

See also @samp{@code{proof-script-comment-start}}.

You should set this variable for reliable working of Proof General.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-comment-end-regexp
@defvar proof-script-comment-end-regexp 
Regexp which matches a comment end in the proof command language.

The default value for this is set as (@code{regexp-quote} @samp{@code{proof-script-comment-end}})
but you can set this variable to something else more precise if necessary.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-case-fold-search
@defvar proof-case-fold-search 
Value for @samp{@code{case-fold-search}} when recognizing portions of proof scripts.@*
Also used for completion, via @samp{@code{proof-script-complete}}.
The default value is nil.  If your prover has a case @strong{insensitive}
input syntax, @samp{@code{proof-case-fold-search}} should be set to t instead.
NB: This setting is not used for matching output from the prover.
@end defvar


Finally, the function @code{proof-looking-at-syntactic-context} is used
internally to help determine the syntactic structure of the buffer.
You can test it to check the settings above.  If necessary, you can
override this with a system-specific function.

@c TEXI DOCSTRING MAGIC: proof-looking-at-syntactic-context
@defun proof-looking-at-syntactic-context 
Determine if current point is at beginning or within comment/string context.@*
If so, return a symbol indicating this ('comment or @code{'string}).
This function invokes <PA-syntactic-context> if that is defined, otherwise
it calls @samp{@code{proof-looking-at-syntactic-context}}.
@end defun
@node Recognizing proofs
@section Recognizing proofs

Several settings each may be supplied for recognizing goal-like and
save-like commands.  The @code{-with-hole-} settings are used to make a
record of the name of the theorem proved.

The @code{-p} subsidiary predicates were added to allow more
discriminating behaviour for particular proof assistants.  (This is a
typical example of where the core framework needs some additional
generalization, to simplify matters, and allow for a smooth handling of
nested proofs; the present state is only part of the way there).


@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp
@defvar proof-goal-command-regexp 
Matches a goal command in the proof script.@*
This is used to make the default value for @samp{@code{proof-goal-command-p}},
used as an important part of script management to find the start
of an atomic undo block.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-goal-command-p
@defvar proof-goal-command-p 
A function to test: is this really a goal command span?

This is added as a more refined addition to @samp{@code{proof-goal-command-regexp}},
to solve the problem that Coq and some other provers can have goals which
look like definitions, etc.  (In the future we may generalize
@samp{@code{proof-goal-command-regexp}} instead).
@end defvar


@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp
@defvar proof-goal-with-hole-regexp 
Regexp which matches a command used to issue and name a goal.@*
The name of the theorem is built from the variable
@samp{@code{proof-goal-with-hole-result}} using the same convention as
for @samp{@code{query-replace-regexp}}.
Used for setting names of goal..save regions and for default
configuration of other modes (function menu, imenu).

It's safe to leave this setting as nil.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-result
@defvar proof-goal-with-hole-result 
How to get theorem name after @samp{@code{proof-goal-with-hole-regexp}} match.@*
String or Int.
If an int N, use @samp{@code{match-string}} to get the value of the Nth parenthesis matched.
If a string, use @samp{@code{replace-match}}.  In this case, @samp{@code{proof-goal-with-hole-regexp}}
should match the entire command.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-save-command-regexp
@defvar proof-save-command-regexp 
Matches a save command.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp
@defvar proof-save-with-hole-regexp 
Regexp which matches a command to save a named theorem.@*
The name of the theorem is built from the variable
@samp{@code{proof-save-with-hole-result}} using the same convention as
@samp{@code{query-replace-regexp}}.
Used for setting names of goal..save and proof regions.

It's safe to leave this setting as nil.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour
@defvar proof-completed-proof-behaviour 
Indicates how Proof General treats commands beyond the end of a proof.@*
Normally goal...save regions are "closed", i.e. made atomic for undo.
But once a proof has been completed, there may be a delay before
the "save" command appears --- or it may not appear at all.  Unless
nested proofs are supported, this can spoil the undo-behaviour in
script management since once a new goal arrives the old undo history
may be lost in the prover.  So we allow Proof General to close
off the goal..[save] region in more flexible ways.
The possibilities are:
@lisp
        nil  -  nothing special; close only when a save arrives
  @code{'closeany}  -  close as soon as the next command arrives, save or not
 @code{'closegoal}  -  close when the next "goal" command arrives
    @code{'extend}  -  keep extending the closed region until a save or goal.
@end lisp
If your proof assistant allows nested goals, it will be wrong to close
off the portion of proof so far, so this variable should be set to nil.

NB: @code{'extend} behaviour is not currently compatible with appearance of
save commands, so don't use that if your prover has save commands.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-really-save-command-p
@defvar proof-really-save-command-p 
Is this really a save command?

This is a more refined addition to @samp{@code{proof-save-command-regexp}}.
It should be a function taking a span and command as argument,
and can be used to track nested proofs.
@end defvar


@node Recognizing other elements
@section Recognizing other elements
@vindex proof-goal-with-hole-regexp
@vindex proof-goal-with-hole-result

To configure @i{Imenu} (which in turn configures @i{Speedbar}), 
you may use the following setting.  If this is unset, a generic
setting based on @code{proof-goal-with-hole-regexp} is configured.

@c TEXI DOCSTRING MAGIC: proof-script-imenu-generic-expression
@defvar proof-script-imenu-generic-expression 
Regular expressions to help find definitions and proofs in a script.@*
Value for @samp{@code{imenu-generic-expression}}, see documentation of Imenu
and that variable for details.
@end defvar

@c This is _not_ docstring magic, but docstring-by-hand from 
@c imenu.el in XEmacs 21.4.12
@defvar imenu-generic-expression
The regex pattern to use for creating a buffer index.

If non-nil this pattern is passed to @samp{imenu--generic-function}
to create a buffer index.

The value should be an alist with elements that look like this:
@lisp
 (@var{menu-title} @var{regexp} @var{index})
@end lisp
or like this:
@lisp
 (@var{menu-title} @var{regexp} @var{index} @var{function} ARGUMENTS...)
@end lisp
with zero or more ARGUMENTS.  The former format creates a simple element in
the index alist when it matches; the latter creates a special element
of the form  (@var{name} @var{function} @var{position-marker} ARGUMENTS...)
with @var{function} and @var{arguments} beiong copied from @samp{imenu-generic-expression}.

@var{menu-title} is a string used as the title for the submenu or nil if the
entries are not nested.

@var{regexp} is a regexp that should match a construct in the buffer that is
to be displayed in the menu; i.e., function or variable definitions,
etc.  It contains a substring which is the name to appear in the
menu.  See the info section on Regexps for more information.

@var{index} points to the substring in @var{regexp} that contains the name (of the
function, variable or type) that is to appear in the menu.

The variable is buffer-local.

The variable @samp{imenu-case-fold-search} determines whether or not the
regexp matches are case sensitive. and @samp{imenu-syntax-alist} can be
used to alter the syntax table for the search.

For example, see the value of @samp{lisp-imenu-generic-expression} used by
@samp{lisp-mode} and @samp{emacs-lisp-mode} with @samp{imenu-syntax-alist} set
locally to give the characters which normally have \"punctuation\"
syntax \"word\" syntax during matching."
@end defvar




@node Configuring undo behaviour
@section Configuring undo behaviour

The settings here are used to configure the way "undo" commands are
calculated.

@c TEXI DOCSTRING MAGIC: proof-non-undoables-regexp
@defvar proof-non-undoables-regexp 
Regular expression matching commands which are @strong{not} undoable.@*
These are commands which should not appear in proof scripts,
for example, undo commands themselves (if the proof assistant
cannot "redo" an "undo").
Used in default functions @samp{@code{proof-generic-state-preserving-p}}
and @samp{@code{proof-generic-count-undos}}.  If you don't use those,
may be left as nil.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-undo-n-times-cmd
@defvar proof-undo-n-times-cmd 
Command to undo n steps of the currently open goal.@*
String or function.
If this is set to a string, @samp{%s} will be replaced by the number of
undo steps to issue.
If this is set to a function, it should return a list of
the appropriate commands (given the number of undo steps).

This setting is used for the default @samp{@code{proof-generic-count-undos}}.
If you set @samp{@code{proof-count-undos-fn}} to some other function, there is no
need to set this variable.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count
@defvar proof-ignore-for-undo-count 
Matcher for script commands to be ignored in undo count.@*
May be left as nil, in which case it will be set to
@samp{@code{proof-non-undoables-regexp}}.
Used in default function @samp{@code{proof-generic-count-undos}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-count-undos-fn
@defvar proof-count-undos-fn 
Function to calculate a list of commands to undo to reach a target span.@*
The function takes a span as an argument, and should return a string
which is the command to undo to the target span.  The target is
guaranteed to be within the current (open) proof.
This is an important function for script management.
The default setting @samp{@code{proof-generic-count-undos}} is based on the
settings @samp{@code{proof-non-undoables-regexp}} and
@samp{@code{proof-non-undoables-regexp}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-generic-count-undos
@defun proof-generic-count-undos span
Count number of undos in @var{span}, return commands needed to undo that far.@*
Command is set using @samp{@code{proof-undo-n-times-cmd}}.

A default value for @samp{@code{proof-count-undos-fn}}.

For this function to work properly, you must configure
@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}.
@end defun






@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn
@defvar proof-find-and-forget-fn 
Function to return list of commands to forget to before its argument span.@*
This setting is used to for retraction (undoing) in proof scripts.

It should undo the effect of all settings between its target span
up to (@code{proof-unprocessed-begin}).  This may involve forgetting a number
of definitions, declarations, or whatever.

If return value is nil, it means there is nothing to do.

This is an important function for script management.
Study one of the existing instantiations for examples of how to write it,
or leave it set to the default function @samp{@code{proof-generic-find-and-forget}}
(which see).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-generic-find-and-forget
@defun proof-generic-find-and-forget span
Calculate a forget/undo command to forget back to @var{span}.@*
This is a long-range forget: we know that there is no
open goal at the moment, so forgetting involves unbinding
declarations, etc, rather than undoing proof steps.

This generic implementation assumes it is enough to find the
nearest following span with a @samp{name} property, and retract
that using @samp{@code{proof-forget-id-command}} with the given name.

If this behaviour is not correct, you must customize the function
with something different.
@end defun

@c TEXI DOCSTRING MAGIC: proof-forget-id-command
@defvar proof-forget-id-command 
Command to forget back to a given named span.@*
A string; @samp{%s} will be replaced by the name of the span.

This is only used in the implementation of @samp{@code{proof-generic-find-and-forget}},
you only need to set if you use that function (by not customizing
@samp{@code{proof-find-and-forget-fn}}.
@end defvar

@c TEXI DOCSTRING MAGIC: pg-topterm-goalhyplit-fn
@defvar pg-topterm-goalhyplit-fn 
Function to return cons if point is at a goal/hypothesis/literal.@*
This is used to parse the proofstate output to mark it up for
proof-by-pointing or literal command insertion.  It should return a cons or nil.
First element of the cons is a symbol, @code{'goal'}, @code{'hyp'} or @code{'lit'}.
The second element is a string: the goal, hypothesis, or literal command itself.

If you leave this variable unset, no proof-by-pointing markup
will be attempted.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-kill-goal-command
@defvar proof-kill-goal-command 
Command to kill the currently open goal.

If this is set to nil, PG will expect @samp{@code{proof-find-and-forget-fn}}
to do all the work of retracting to an arbitrary point in a file.
Otherwise, the generic split-phase mechanism will be used:

1. If inside an unclosed proof, use @samp{proof-count-undos}.
2. If retracting to before an unclosed proof, use
@samp{@code{proof-kill-goal-command}}, followed by @samp{@code{proof-find-and-forget-fn}}
if necessary.
@end defvar



@node Nested proofs
@section Nested proofs

Proof General allows configuration for provers which have particular
notions of nested proofs.  The right thing may happen automatically,
or you may need to adjust some of the following settings.

First, you should alter the next setting if the prover retains history
for nested proofs.

@c TEXI DOCSTRING MAGIC: proof-nested-goals-history-p
@defvar proof-nested-goals-history-p 
Whether the prover supports recovery of history for nested proofs.@*
If it does (non-nil), Proof General will retain history inside
nested proofs.
If it does not, Proof General will amalgamate nested proofs into single
steps within the outer proof.
@end defvar
Second, it may happen (i.e. it does for Coq) that the prover has a
history mechanism which necessitates keeping track of the number of
nested "undoable" commands, even if the history of the proof itself is
lost.  

@c TEXI DOCSTRING MAGIC: proof-nested-undo-regexp
@defvar proof-nested-undo-regexp 
Regexp for commands that must be counted in nested goal-save regions.

Used for provers which allow nested atomic goal-saves, but with some
nested history that must be undone specially.

At the moment, the behaviour is that a goal-save span has a @code{'nestedundos}
property which is set to the number of commands within it which match
this regexp.  The idea is that the prover-specific code can create a
customized undo command to retract the goal-save region, based on the
@code{'nestedundos} setting.  Coq uses this to forget declarations, since
declarations in Coq reside in a separate context with its own (flat)
history.
@end defvar


@node Omitting proofs for speed
@section Omitting proofs for speed

In normal operation, the commands in an asserted region are sent
successively to the proof assistant. When the proof assistant
reports an error, processing stops. This ensures the consistency
of the development. Proof General supports omitting portions of
the asserted region to speed processing up at the cost of
consistency. Portions that can be potentially omitted are called
@emph{opaque proofs} in Proof General, because usually only
opaque proofs (in the sense of Coq) can be omitted without
risking to break the following code. This feature is also
described in the Proof General manual, @pxref{Script processing
commands,,,ProofGeneral} and
@pxref{Omitting proofs for speed,,,ProofGeneral}.

The omit proofs feature works in a simple, straightforward way:
After parsing the asserted region, Proof General uses regular
expressions to search for commands that start
(@code{proof-script-proof-start-regexp}) and end
(@code{proof-script-proof-end-regexp}) an opaque proof. If one is
found, the opaque proof is replaced with a cheating command
(@code{proof-script-proof-admit-command}). From this description
it is immediate, that the omit proof feature does only work if
proofs are not nested. If a nested proof is found, a warning is
displayed and omitting proofs stops at that location for the
currently asserted region.

In Coq, commands with non-local effects, such as @code{Hint}, may
appear inside proofs. Additionally, admitting a proof of a @code{Let}
declaration causes a warning in Coq. To treat such cases, the
predicate @code{proof-script-cmd-prevents-proof-omission} is applied
to all commands inside proofs and the regular expression
@code{proof-script-cmd-force-next-proof-kept} is matched against all
commands outside proofs. In case of a hit, the current or,
respectively, the next proof is treated as non-opaque and is not
omitted. Note that a match of
@code{proof-script-cmd-force-next-proof-kept} is only handled if the
matching command and the following proof appear in the same asserted
region. If the proof is asserted separately, the information about the
match in the previously asserted region is lost and the proof may thus
be omitted.

To enable the omit proofs feature, the following settings must be
configured.

@c TEXI DOCSTRING MAGIC: proof-omit-proofs-configured
@defvar proof-omit-proofs-configured 
t if the omit proofs feature has been configured by the proof assitant.@*
See also @samp{@code{proof-omit-proofs-option}} or the Proof General manual
for a description of the feature. This option can only be set, if
all of @samp{@code{proof-script-proof-start-regexp}},
@samp{@code{proof-script-proof-end-regexp}},
@samp{@code{proof-script-definition-end-regexp}} and
@samp{@code{proof-script-proof-admit-command}} have been configured.

The omit proofs feature skips over opaque proofs in the source
code, admitting the theorems, to speed up processing.

If @samp{@code{proof-omit-proofs-option}} is set by the user, all proof
commands in the source following a match of
@samp{@code{proof-script-proof-start-regexp}} up to and including the next
match of @samp{@code{proof-script-proof-end-regexp}}, are omitted (not send
to the proof assistant) and replaced by
@samp{@code{proof-script-proof-admit-command}}. If a match for
@samp{@code{proof-script-definition-end-regexp}} is found while searching
forward for the proof end or if
@samp{@code{proof-script-cmd-prevents-proof-omission}} recognizes a proof
command that prevents proof omission then the current proof (up
to and including the match of
@samp{@code{proof-script-definition-end-regexp}} or
@samp{@code{proof-script-proof-end-regexp}}) is considered to be not opaque
and not omitted, thus all these proof commands _are_ sent to the
proof assistant.

The feature does not work for nested proofs. If a match for
@samp{@code{proof-script-proof-start-regexp}} is found before the next match
for @samp{@code{proof-script-proof-end-regexp}} or
@samp{@code{proof-script-definition-end-regexp}}, the search for opaque
proofs immediately stops and all commands following the previous
match of @samp{@code{proof-script-proof-start-regexp}} are sent verbatim to
the proof assistant.

All the regular expressions for this feature are matched against
the commands inside proof action items, that is as strings,
without surrounding space.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-proof-start-regexp
@defvar proof-script-proof-start-regexp 
Regular expression for the start of a proof for the omit proofs feature.@*
See @samp{@code{proof-omit-proofs-configured}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-proof-end-regexp
@defvar proof-script-proof-end-regexp 
Regular expression for the end of an opaque proof for the omit proofs feature.@*
See @samp{@code{proof-omit-proofs-configured}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-definition-end-regexp
@defvar proof-script-definition-end-regexp 
Regexp for the end of a non-opaque proof for the omit proofs feature.@*
See @samp{@code{proof-omit-proofs-configured}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-proof-admit-command
@defvar proof-script-proof-admit-command 
Proof command to be inserted instead of omitted proofs.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-cmd-prevents-proof-omission
@defvar proof-script-cmd-prevents-proof-omission 
Optional predicate to match commands that prevent omitting the current proof.@*
If set, this option should contain a function that takes a proof
command (as string) as argument and returns t or nil. If set, the
function is called on every proof command inside a proof while
scanning for proofs to omit. The predicate should return t if the
command has effects ouside the proof, potentially breaking the
script if the current proof is omitted. If the predicate returns
t, the proof is considered to be not opaque and thus not omitted.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-script-cmd-force-next-proof-kept
@defvar proof-script-cmd-force-next-proof-kept 
Optional regexp for commands that prevent omitting the next proof.@*
If set, this option should contain a regular expression that
matches proof-script commands that prevent the omission of proofs
dirctly following this command. When scanning the newly asserted
region for proofs to omit, every proof-script command outside
proofs is matched against this regexp. If it matches and the next
command matches @samp{@code{proof-script-proof-start-regexp}} this following
proof will not be omitted.

Note that recognition of commands with this regular expression
does only work if the command and the following proof are
asserted together.
@end defvar

@node Safe (state-preserving) commands
@section Safe (state-preserving) commands

A proof command is "safe" if it can be issued away from the proof
script.  For this to work it should be state-preserving in the proof
assistant (with respect to an on-going proof).

@c TEXI DOCSTRING MAGIC: proof-state-preserving-p
@defvar proof-state-preserving-p 
A predicate, non-nil if its argument (a command) preserves the proof state.@*
This is a safety-test used by @samp{@code{proof-minibuffer-cmd}} to filter out scripting
commands which should be entered directly into the script itself.

The default setting for this function, @samp{@code{proof-generic-state-preserving-p}}
tests by negating the match on @samp{@code{proof-non-undoables-regexp}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-generic-state-preserving-p
@defun proof-generic-state-preserving-p cmd
Is @var{cmd} state preserving?  Match on @samp{@code{proof-non-undoables-regexp}}.
@end defun


@node Activate scripting hook
@section Activate scripting hook


@c TEXI DOCSTRING MAGIC: proof-activate-scripting-hook
@defvar proof-activate-scripting-hook 
Hook run when a buffer is switched into scripting mode.@*
The current buffer will be the newly active scripting buffer.

This hook may be useful for synchronizing with the proof
assistant, for example, to switch to a new theory
(in case that isn't already done by commands in the proof
script).

When functions in this hook are called, the variable
@samp{activated-interactively} will be non-nil if
@samp{@code{proof-activate-scripting}} was called interactively
(rather than as a side-effect of some other action).
If a hook function sends commands to the proof process,
it should wait for them to complete (so the queue is cleared
for scripting commands), unless activated-interactively is set.
@end defvar


@node Automatic multiple files
@section Automatic multiple files

@xref{Handling Multiple Files}, for more details about this
setting.

@c TEXI DOCSTRING MAGIC: proof-auto-multiple-files
@defvar proof-auto-multiple-files 
Whether to use automatic multiple file management.@*
If non-nil, Proof General will automatically retract a script file
whenever another one is retracted which it depends on.  It assumes
a simple linear dependency between files in the order which
they were processed.

If your proof assistant has no management of file dependencies, or one
which depends on a simple linear context, you may be able to use this
setting to good effect.  If the proof assistant has more complex
file dependencies then you should configure it to communicate with
Proof General about the dependencies rather than using this setting.
@end defvar

@node Completely asserted buffers
@section Completely asserted buffers

When switching scripting from buffer A to buffer B Proof General
normally offers the choice of either completely retracting or
completely asserting buffer A. The option to completely assert
buffer A is offered, because the material in B may depend on A.
Even if B does not depend on A, it does no harm if one keeps the
development of A loaded in the proof assistant. This observation
is true for many proof assistants.

One exception is Coq. Assume file B depends on file A. When Coq
processes B it does not read the sources of A. Instead it loads a
compiled object representation of A. Therefore, when switching
from A to B, it does make no sense to keep the material of A
loaded in the proof assistant. For Coq, the material of A may
even provoke errors on correct input. Therefore, for coq, the
right behaviour is to completely retract buffer A before
switching to B. 

@c TEXI DOCSTRING MAGIC: proof-no-fully-processed-buffer
@defvar proof-no-fully-processed-buffer 
Set to t if buffers should always retract before scripting elsewhere.@*
Leave at nil if fully processed buffers make sense for the current
proof assistant.  If nil the user can choose to fully assert a
buffer when starting scripting in a different buffer.  If t there
is only the choice to fully retract the active buffer before
starting scripting in a different buffer.  This last behavior is
needed for Coq.
@end defvar



@node Completions
@section Completions

Proof General allows provers to create a @i{completion table} to help
writing keywords and identifiers in proof scripts.  This is documented
in the main @i{Proof General} user manual but summarized here for (a
different kind of) completion.

Completions are filled in according to what has been recently typed,
from a database of symbols.  The database is automatically saved at the
end of a session.  Completion is usually a hand-wavy thing, so we don't
make any attempt to maintain a precise completion table or anything.

The completion table maintained by @file{complete.el} is initialized
from @code{PA-completion-table} when @file{proof-script.el} is loaded.
This is done with the function @code{proof-add-completions} which
you may want to call at other times.


@c TEXI DOCSTRING MAGIC: PA-completion-table
@defvar PA-completion-table 
List of identifiers to use for completion for this proof assistant.@*
Completion is activated with M-x complete.

If this table is empty or needs adjusting, please make changes using
@samp{@code{customize-variable}} and post suggestions at
https://github.com/ProofGeneral/PG/issues
@end defvar

@c TEXI DOCSTRING MAGIC: proof-add-completions
@deffn Command proof-add-completions 
Add completions from <PA>-completion-table to completion database.@*
Uses @samp{@code{add-completion}} with a negative number of uses and ancient
last use time, to discourage saving these into the users database.
@end deffn






@node Proof Shell Settings
@chapter Proof Shell Settings

The variables in this chapter concern the proof shell mode, and are the
largest group.  They are split into several subgroups.  The first
subgroup are commands invoked at various points.  The second subgroup of
variables are concerned with matching the output from the proof
assistant.  The final subgroup contains various hooks which you can set
to add lisp customization to Proof General in various points (some of
them are also used internally for behaviour you may wish to adjust).

Variables for configuring the proof shell are put into the customize
group @code{proof-shell}.

These should be set in the shell mode configuration, before
@code{proof-shell-config-done} is called.

To understand the way the proof assistant runs inside Emacs, you may
want to refer to the @code{comint.el} (Command interpreter) package
distributed with Emacs.  This package controls several shell-like modes
available in Emacs, including the @code{proof-shell-mode} and
all specific shell modes derived from it.

@menu
* Proof shell commands::
* Script input to the shell::
* Settings for matching various output from proof process::
* Settings for matching urgent messages from proof process::
* Hooks and other settings::  
@end menu

@node Proof shell commands
@section Commands

Settings in this section configure Proof General with commands
to send to the prover to activate certain actions.

@c TEXI DOCSTRING MAGIC: proof-prog-name
@defvar proof-prog-name 
System command to run the proof assistant in the proof shell.@*
May contain arguments separated by spaces, but see also the
prover specific settings @samp{<PA>-prog-args} and @samp{<PA>-prog-env}.

Remark: if @samp{<PA>-prog-args} is non-nil, then @samp{@code{proof-prog-name}} is considered
strictly: it must contain @strong{only} the program name with no option, spaces
are interpreted literally as part of the program name.
@end defvar

@c TEXI DOCSTRING MAGIC: PA-prog-args
@defvar PA-prog-args 
Arguments to be passed to @samp{@code{proof-prog-name}} to run the proof assistant.@*
If non-nil, will be treated as a list of arguments for @samp{@code{proof-prog-name}}.
Otherwise @samp{@code{proof-prog-name}} will be split on spaces to form arguments.

Remark: Arguments are interpreted strictly: each one must contain only one
word, with no space (unless it is the same word). For example if the
arguments are -x foo -y bar, then the list should be '("-x" "foo"
"-y" "bar"), notice that '("-x foo" "-y bar") is @strong{wrong}.
@end defvar

@c TEXI DOCSTRING MAGIC: PA-prog-env
@defvar PA-prog-env 
Modifications to @samp{@code{process-environment}} made before running @samp{@code{proof-prog-name}}.@*
Each element should be a string of the form ENVVARNAME=@var{value}.  They will be
added to the environment before launching the prover (but not pervasively).
For example for coq on Windows you might need something like:
(setq @code{coq-prog-env} '("HOME=C:\Program Files\Coq\"))
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands
@defvar proof-shell-auto-terminate-commands 
Non-nil if Proof General should try to add terminator to every command.@*
If non-nil, whenever a command is sent to the prover using
@samp{@code{proof-shell-invisible-command}}, Proof General will check to see if it
ends with @samp{@code{proof-terminal-string}}, and add it if not.
If @samp{@code{proof-terminal-string}} is nil, this has no effect.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd
@defvar proof-shell-pre-sync-init-cmd 
The command for configuring the proof process to gain synchronization.@*
This command is sent before Proof General's synchronization
mechanism is engaged, to allow customization inside the process
to help gain syncrhonization (e.g. engaging special markup).

It is better to configure the proof assistant for this purpose
via command line options if possible, in which case this variable
does not need to be set.

See also @samp{@code{proof-shell-init-cmd}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd
@defvar proof-shell-init-cmd 
The command(s) for initially configuring the proof process.@*
This command is sent to the process as soon as synchronization is gained
(when an annotated prompt is first recognized).  It can be used to configure
the proof assistant in some way, or print a welcome message
(since output before the first prompt is discarded).

See also @samp{@code{proof-shell-pre-sync-init-cmd}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
@defvar proof-shell-restart-cmd 
A command for re-initialising the proof process.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd
@defvar proof-shell-quit-cmd 
A command to quit the proof process.  If nil, send EOF instead.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd
@defvar proof-shell-cd-cmd 
Command to the proof assistant to change the working directory.@*
The format character @samp{%s} is replaced with the directory, and
the escape sequences in @samp{@code{proof-shell-filename-escapes}} are
applied to the filename.

This setting is used to define the function @samp{@code{proof-cd}} which
changes to the value of (@code{default-directory}) for script buffers.
For files, the value of (@code{default-directory}) is simply the
directory the file resides in.

NB: By default, @samp{@code{proof-cd}} is called from @samp{@code{proof-activate-scripting-hook}},
so that the prover switches to the directory of a proof
script every time scripting begins.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-start-silent-cmd
@defvar proof-shell-start-silent-cmd 
Command to turn prover goals output off when sending many script commands.@*
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
See also @samp{@code{proof-shell-stop-silent-cmd}}.
NB: terminator not added to command.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-stop-silent-cmd
@defvar proof-shell-stop-silent-cmd 
Command to turn prover output on.@*
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
See also @samp{@code{proof-shell-start-silent-cmd}}.
NB: Terminator not added to command.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-silent-threshold
@defvar proof-shell-silent-threshold 
Number of waiting commands in the proof queue needed to trigger silent mode.@*
Default is 2, but you can raise this in case switching silent mode
on or off is particularly expensive (or make it ridiculously large
to disable silent mode altogether).
@end defvar
@xref{Handling Multiple Files},
for more details about the final two settings in this group,


@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd
@defvar proof-shell-inform-file-processed-cmd 
Command to the proof assistant to tell it that a file has been processed.@*
The format character @samp{%s} is replaced by a complete filename for a
script file which has been fully processed interactively with
Proof General.  See @samp{@code{proof-format-filename}} for other possibilities
to process the filename.

This setting used to interface with the proof assistant's internal
management of multiple files, so the proof assistant is kept aware of
which files have been processed.  Specifically, when scripting
is deactivated in a completed buffer, it is added to Proof General's
list of processed files, and the prover is told about it by
issuing this command.

If this is set to nil, no command is issued.

See also: @samp{@code{proof-shell-inform-file-retracted-cmd}},
@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd
@defvar proof-shell-inform-file-retracted-cmd 
Command to the proof assistant to tell it that a file has been retracted.@*
The format character @samp{%s} is replaced by a complete filename for a
script file which Proof General wants the prover to consider as not
completely processed.  See @samp{@code{proof-format-filename}} for other
possibilities to process the filename.

This is used to interface with the proof assistant's internal
management of multiple files, so the proof assistant is kept aware of
which files have been processed.  Specifically, when scripting
is activated, the file is removed from Proof General's list of
processed files, and the prover is told about it by issuing this
command.  The action may cause the prover in turn to suggest to
Proof General that files depending on this one are
also unlocked.

If this is set to nil, no command is issued.

It is also possible to set this value to a function which will
be invoked on the name of the retracted file, and should remove
the ancestor files from @samp{@code{proof-included-files-list}} by some
other calculation.

See also: @samp{@code{proof-shell-inform-file-processed-cmd}},
@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}.
@end defvar


@node Script input to the shell
@section Script input to the shell

Generally, commands from the proof script are sent verbatim to the proof
process running in the proof shell.  For historical reasons, carriage
returns are stripped by default.  You can set
@code{proof-shell-strip-crs-from-input} to adjust that.  For more
sophisticated pre-processing of the sent string, you may like to set
@code{proof-shell-insert-hook}.

@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-input 
@defvar proof-shell-strip-crs-from-input 
If non-nil, replace carriage returns in every input with spaces.@*
This is enabled by default: it is appropriate for many systems
based on human input, because several CR's can result in several
prompts, which may mess up the display (or even worse, the
synchronization).

If the prover can be set to output only one prompt for every chunk of
input, then newlines can be retained in the input.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-insert-hook
@defvar proof-shell-insert-hook 
Hook run by @samp{@code{proof-shell-insert}} before inserting a command.@*
Can be used to configure the proof assistant to the interface in
various ways -- for example, to observe or alter the commands sent to
the prover, or to sneak in extra commands to configure the prover.

This hook is called inside a @samp{@code{save-excursion}} with the @samp{@code{proof-shell-buffer}}
current, just before inserting and sending the text in the
variable @samp{string}.  The hook can massage @samp{string} or insert additional
text directly into the @samp{@code{proof-shell-buffer}}.
Before sending @samp{string}, it will be stripped of carriage returns.

Additionally, the hook can examine the variable @samp{action}.  It will be
a symbol, set to the callback command which is executed in the proof
shell filter once @samp{string} has been processed.  The @samp{action} variable
suggests what class of command is about to be inserted, the first two
are normally the ones of interest:
@lisp
 @code{'proof-done-advancing}       A "forward" scripting command
 @code{'proof-done-retracting}      A "backward" scripting command
 @code{'proof-done-invisible}       A non-scripting command
 @code{'proof-shell-set-silent}     Indicates prover output has been surpressed
 @code{'proof-shell-clear-silent}   Indicates prover output has been restored
 @code{'init-cmd}                   Early initialization command sent to prover
@end lisp
Caveats: You should be very careful about setting this hook.  Proof
General relies on a careful synchronization with the process between
inputs and outputs.  It expects to see a prompt for each input it
sends from the queue.  If you add extra input here and it causes more
prompts than expected, things will break!  Extending the variable
@samp{string} may be safer than inserting text directly, since it is
stripped of carriage returns before being sent.

Example uses:
Lego used this hook for setting the pretty printer width if
the window width has changed;
Plastic used it to remove literate-style markup from @samp{string}.

See also @samp{@code{proof-script-preprocess}} which can munge text when
it is added to the queue of commands.
@end defvar






@node Settings for matching various output from proof process
@section Settings for matching various output from proof process

These settings control the way Proof General reacts to process output.
The single most important setting is
@code{proof-shell-annotated-prompt-regexp}, which @b{must} be set as
part of the prover configuraton.  This is used to configure the
communication with the prover process.

@c TEXI DOCSTRING MAGIC: pg-subterm-first-special-char
@defvar pg-subterm-first-special-char 
First special character.@*
Codes above this character can have special meaning to Proof General,
and are stripped from the prover's output strings.
Leave unset if no special characters are being used.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp
@defvar proof-shell-annotated-prompt-regexp 
Regexp matching a (possibly annotated) prompt pattern.

@var{this} IS THE @var{most} @var{important} @var{setting} TO @var{configure}!!

Output is grabbed between pairs of lines matching this regexp,
and the appearance of this regexp is used by Proof General to
recognize when the prover has finished processing a command.

To help speed up matching you may be able to annotate the
proof assistant prompt with a special character not appearing
in ordinary output, which should appear in this regexp.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-error-regexp
@defvar proof-shell-error-regexp 
Regexp matching an error report from the proof assistant.

We assume that an error message corresponds to a failure in the last
proof command executed.  So don't match mere warning messages with
this regexp.  Moreover, an error message should @strong{not} be matched as an
eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it
will be lost.

Error messages are considered to begin from @samp{@code{proof-shell-error-regexp}}
and continue until the next prompt.  The variable
@samp{@code{proof-shell-truncate-before-error}} controls whether text before the
error message is displayed.

The engine matches interrupts before errors, see @samp{@code{proof-shell-interrupt-regexp}}.

It is safe to leave this variable unset (as nil).
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp
@defvar proof-shell-interrupt-regexp 
Regexp matching output indicating the assistant was interrupted.@*
We assume that an interrupt message corresponds to a failure in the last
proof command executed.  So don't match mere warning messages with
this regexp.  Moreover, an interrupt message should not be matched as an
eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it
will be lost.

The engine matches interrupts before errors, see @samp{@code{proof-shell-error-regexp}}.

It is safe to leave this variable unset (as nil).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-truncate-before-error
@defvar proof-shell-truncate-before-error 
Non-nil means truncate output that appears before error messages.@*
If nil, the whole output that the prover generated before the last
error message will be shown.

NB: the default setting for this is t to be compatible with
behaviour in Proof General before version 3.4.  The more obvious
setting for new instances is probably nil.

Interrupt messages are treated in the same way.
See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt-regexp}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp
@defvar proof-shell-proof-completed-regexp 
Regexp matching output indicating a finished proof.

When output which matches this regexp is seen, we clear the goals
buffer in case this is not also marked up as a @samp{goals} type of
message.

We also enable the QED function (save a proof) and we may automatically
close off the proof region if another goal appears before a save
command, depending on whether the prover supports nested proofs or not.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp
@defvar proof-shell-start-goals-regexp 
Regexp matching the start of the proof state output.@*
This is an important setting.  Output between @samp{@code{proof-shell-start-goals-regexp}}
and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
and possibly analysed further for proof-by-pointing markup.
If it is left as nil, the goals buffer will not be used.

The goals display starts at the beginning of the match on this
regexp, unless it has a match group, in which case it starts
at (@code{match-end} 1).
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
@defvar proof-shell-end-goals-regexp 
Regexp matching the end of the proof state output, or nil.@*
This allows a shorter form of the proof state output to be displayed,
in case several messages are combined in a command output.

The portion treated as the goals output will be that between the
match on @samp{@code{proof-shell-start-goals-regexp}} (which see) and the
start of the match on @samp{@code{proof-shell-end-goals-regexp}}.

If nil, use the whole of the output from the match on
@samp{@code{proof-shell-start-goals-regexp}} up to the next prompt.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp
@defvar proof-shell-assumption-regexp 
A regular expression matching the name of assumptions.

At the moment, this setting is not used in the generic Proof General.

Future use may provide a generic implementation for @samp{@code{pg-topterm-goalhyplit-fn}},
used to help parse the goals buffer to annotate it for proof by pointing.
@end defvar



@node Settings for matching urgent messages from proof process
@section Settings for matching urgent messages from proof process

Among the various dialogue messages that the proof assistant outputs
during proof, Proof General can consider certain messages to be
"urgent".  When processing many lines of a proof, Proof General will
normally supress the output, waiting until the final message appears
before displaying anything to the user.  Urgent messages escape this:
typically they include messages that the prover wants the user to
notice, for example, perhaps, file loading messages, timing
statistics or dedicated tracing messages which can be sent to the
@code{*trace*} buffer.

So that Proof General notices, these urgent messages should be marked-up
with "eager" annotations.

@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start
@defvar proof-shell-eager-annotation-start 
Eager annotation field start.  A regular expression or nil.@*
An "eager annotation indicates" to Proof General that some following output
should be displayed (or processed) immediately and not accumulated for
parsing later.  Note that this affects processing of output which is
ordinarily accumulated: output which appears before the eager annotation
start will be discarded.

The start/end annotations can be used to hilight the output, but
are stripped from display of the message in the minibuffer.

It is useful to recognize (starts of) warnings or file-reading messages
with this regexp.  You must also recognize any special messages
from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}},
@samp{@code{proof-shell-retract-files-regexp}}, etc.)

See also @samp{@code{proof-shell-eager-annotation-start-length}},
@samp{@code{proof-shell-eager-annotation-end}}.

Set to nil to disable this feature.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start-length
@defvar proof-shell-eager-annotation-start-length 
Maximum length of an eager annotation start.@*
Must be set to the maximum length of the text that may match
@samp{@code{proof-shell-eager-annotation-start}} (at least 1).
If this value is too low, eager annotations may be lost!

This value is used internally by Proof General to optimize the process
filter to avoid unnecessary searching.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end
@defvar proof-shell-eager-annotation-end 
Eager annotation field end.  A regular expression or nil.@*
An eager annotation indicates to Emacs that some following output
should be displayed or processed immediately.

See also @samp{@code{proof-shell-eager-annotation-start}}.

It is nice to recognize (ends of) warnings or file-reading messages
with this regexp.  You must also recognize (ends of) any special messages
from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}},
@samp{@code{proof-shell-retract-files-regexp}}, etc.)

The default value is "\n" to match up to the end of the line.
@end defvar


The default action for urgent messages is to display them in the
response buffer, highlighted.  But we also allow for some control
messages, issued from the proof assistant to Proof General and not
intended for the user to see.  These are recognized in the same way as
urgent messages (marked with eager annotations), so they will
be acted on as soon as they are issued by the prover.


@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp
@defvar proof-shell-clear-response-regexp 
Regexp matching output telling Proof General to clear the response buffer.

More precisely, this should match a string which is bounded by
matches on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.

This feature is useful to give the prover more control over what output
is shown to the user.  Set to nil to disable.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-clear-goals-regexp
@defvar proof-shell-clear-goals-regexp 
Regexp matching output telling Proof General to clear the goals buffer.

More precisely, this should match a string which is bounded by
matches on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.

This feature is useful to give the prover more control over what output
is shown to the user.  Set to nil to disable.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-interactive-prompt-regexp
@defvar proof-shell-interactive-prompt-regexp 
Matches output from the prover which indicates an interactive prompt.@*
If we match this, we suppose that the prover has switched to an
interactive diagnostic mode which requires direct interaction
with the shell rather than via script management.  In this case,
the shell buffer will be displayed and the user left to their own
devices.

Note: this should match a string which is bounded by matches
on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-trace-output-regexp
@defvar proof-shell-trace-output-regexp 
Matches tracing output which should be displayed in trace buffer.@*
Each line which matches this regexp but would otherwise be treated
as an ordinary response, is sent to the trace buffer instead of the
response buffer.

This is intended for unusual debugging output from
the prover, rather than ordinary output from final proofs.

This should match a string which is bounded by matches
on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.

Set to nil to disable.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-theorem-dependency-list-regexp
@defvar proof-shell-theorem-dependency-list-regexp 
Matches output telling Proof General about dependencies.@*
This is to allow navigation and display of dependency information.
The output from the prover should be a message with the form
@lisp
   @var{dependencies} OF  X Y Z   ARE  A B C
@end lisp
with X Y Z, A B C separated by whitespace or somehow else (see
@samp{@code{proof-shell-theorem-dependency-list-split}}.  This variable should
be set to a regexp to match the overall message (which should
be an urgent message), with two sub-matches for X Y Z and A B C.

This is an experimental feature, currently work-in-progress.
@end defvar

Two important control messages are recognized by
@code{proof-shell-process-file} and
@code{proof-shell-retract-files-regexp}, used for synchronizing Proof
General with a file loading mechanism built into the proof assistant.
@xref{Handling Multiple Files}, for more details about how to use the
final four settings described here.

@vindex proof-included-files-list
@c TEXI DOCSTRING MAGIC: proof-shell-process-file
@defvar proof-shell-process-file 
A pair (@var{regexp} . @var{function}) to match a processed file name.

If @var{regexp} matches output, then the function @var{function} is invoked.
It must return the name of a script file (with complete path)
that the system has successfully processed.  In practice,
@var{function} is likely to inspect the match data.  If it returns
the empty string, the file name of the scripting buffer is used
instead.  If it returns nil, no action is taken.

More precisely, @var{regexp} should match a string which is bounded by
matches on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.

Care has to be taken in case the prover only reports on compiled
versions of files it is processing.  In this case, @var{function} needs to
reconstruct the corresponding script file name.  The new (true) file
name is added to the front of @samp{@code{proof-included-files-list}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp
@defvar proof-shell-retract-files-regexp 
Matches a message that the prover has retracted a file.

More precisely, this should match a string which is bounded by
matches on @samp{@code{proof-shell-eager-annotation-start}} and
@samp{@code{proof-shell-eager-annotation-end}}.

At this stage, Proof General's view of the processed files is out of
date and needs to be updated with the help of the function
@samp{@code{proof-shell-compute-new-files-list}}.
@end defvar
@vindex proof-included-files-list

@c TEXI DOCSTRING MAGIC: proof-shell-compute-new-files-list
@defvar proof-shell-compute-new-files-list 
Function to update @samp{proof-included-files list}.

It needs to return an up-to-date list of all processed files.  The
result will be stored in @samp{@code{proof-included-files-list}}.

This function is called when @samp{@code{proof-shell-retract-files-regexp}}
has been matched in the prover output.

In practice, this function is likely to inspect the
previous (global) variable @samp{@code{proof-included-files-list}} and the
match data triggered by @samp{@code{proof-shell-retract-files-regexp}}.
@end defvar


@c TEXI DOCSTRING MAGIC: proof-cannot-reopen-processed-files
@defvar proof-cannot-reopen-processed-files 
Non-nil if the prover allows re-opening of already processed files.

If the user has used Proof General to process a file incrementally,
then PG will retain the spans recording undo history in the buffer
corresponding to that file (provided it remains visited in Emacs).

If the prover allows, it will be possible to undo to a position within
this file.  If the prover does @strong{not} allow this, this variable should
be set non-nil, so that when a completed file is activated for
scripting (to do undo operations), the whole history is discarded.
@end defvar





@node Hooks and other settings
@section Hooks and other settings

@c TEXI DOCSTRING MAGIC: proof-shell-filename-escapes
@defvar proof-shell-filename-escapes 
A list of escapes that are applied to %s for filenames.@*
A list of cons cells, car of which is string to be replaced
by the cdr.
For example, when directories are sent to Isabelle, HOL, and Coq,
they appear inside ML strings and the backslash character and
quote characters must be escaped.  The setting
@lisp
  '(("@var{\\\\}" . "@var{\\\\}")
    ("\"" . "\\\""))
@end lisp
achieves this.

This setting is used inside the function @samp{@code{proof-format-filename}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type
@defvar proof-shell-process-connection-type 
The value of @samp{@code{process-connection-type}} for the proof shell.@*
Set non-nil for ptys, nil for pipes.

@var{note}: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
good choice: input is cut after @var{4095} chars, which hangs pg.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook
@defvar proof-shell-handle-error-or-interrupt-hook 
Run after an error or interrupt has been reported in the response buffer.@*
Hook functions may inspect @samp{@code{proof-shell-last-output-kind}} to
determine whether the cause was an error or interrupt.  Possible
values for this hook include:
@lisp
 @samp{@code{proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window}}
 @samp{@code{proof-goto-end-of-locked-if-pos-not-visible-in-window}}
@end lisp
which move the cursor in the scripting buffer on an error or
error/interrupt.

Remark: This hook is called from shell buffer.  If you want to do
something in scripting buffer, @samp{@code{save-excursion}} and/or @samp{@code{set-buffer}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook
@defvar proof-shell-pre-interrupt-hook 
Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@*
This hook is added to allow customization for systems that query the user
before returning to the top level.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-handle-output-system-specific
@defvar proof-shell-handle-output-system-specific 
Set this variable to handle system specific output.@*
Errors and interrupts are recognised in the function
@samp{@code{proof-shell-handle-immediate-output}}.  Later output is
handled by @samp{@code{proof-shell-handle-delayed-output}}, which
displays messages to the user in @strong{goals} and @strong{response}
buffers.

This hook can run between the two stages to take some effect.

It should be a function which is passed (cmd string) as
arguments, where @samp{cmd} is a string containing the currently
processed command and @samp{string} is the response from the proof
system.  If action is taken and goals/response display should
be prevented, the function should update the variable
@samp{@code{proof-shell-last-output-kind}} to some non-nil symbol.

The symbol will be compared against standard ones, see documentation
of @samp{@code{proof-shell-last-output-kind}}.  A suggested canonical non-standard
symbol is @code{'systemspecific}.
@end defvar





@node Goals Buffer Settings
@chapter Goals Buffer Settings

The goals buffer settings allow configuration of Proof General for proof
by pointing or similar features.
See the Proof General @uref{https://proofgeneral.github.io/doc, documentation web page}
for a link to the technical report ECS-LFCS-97-368 which hints
at how to use these settings.

@c At the moment these settings are disabled.

@c TEXI DOCSTRING MAGIC: pg-goals-change-goal
@defvar pg-goals-change-goal 
Command to change to the goal @samp{%s}.
@end defvar
@c TEXI FIX DOCSTRING MAGIC: pbp-goal-command
@defvar pbp-goal-command 
Command sent when @samp{pg-goals-button-action} is requested on a goal.
@end defvar
@c TEXI FIX DOCSTRING MAGIC: pbp-hyp-command
@defvar pbp-hyp-command 
Command sent when @samp{pg-goals-button-action} is requested on an assumption.
@end defvar
@c TEXI DOCSTRING MAGIC: pg-goals-error-regexp
@defvar pg-goals-error-regexp 
Regexp indicating that the proof process has identified an error.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-result-start
@defvar proof-shell-result-start 
Regexp matching start of an output from the prover after pbp commands.@*
In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-result-end
@defvar proof-shell-result-end 
Regexp matching end of output from the prover after pbp commands.@*
In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
@end defvar

@c TEXI DOCSTRING MAGIC: pg-subterm-start-char
@defvar pg-subterm-start-char 
Opening special character for subterm markup.@*
Subsequent special characters with values @strong{below}
@samp{@code{pg-subterm-first-special-char}} are assumed to be subterm position
indicators.  Annotations should be finished with @samp{@code{pg-subterm-sep-char}};
the end of the concrete syntax is indicated by @samp{@code{pg-subterm-end-char}}.

If @samp{@code{pg-subterm-start-char}} is nil, subterm markup is disabled.
@end defvar
@c TEXI DOCSTRING MAGIC: pg-subterm-sep-char
@defvar pg-subterm-sep-char 
Finishing special for a subterm markup.@*
See doc of @samp{@code{pg-subterm-start-char}}.
@end defvar
@c TEXI DOCSTRING MAGIC: pg-topterm-regexp
@defvar pg-topterm-regexp 
Annotation regexp that indicates the beginning of a "top" element.@*
A "top" element may be a sub-goal to be proved or a named hypothesis,
for example.  It could also be a literal command to insert and
send back to the prover.

The function @samp{@code{pg-topterm-goalhyplit-fn}} examines text following this
special character, to determine what kind of top element it is.

This setting is also used to see if proof-by-pointing features
are configured.  If it is unset, some of the code
for parsing the prover output is disabled.
@end defvar
@c TEXI DOCSTRING MAGIC: pg-subterm-end-char
@defvar pg-subterm-end-char 
Closing special character for subterm markup.@*
See @samp{@code{pg-subterm-start-char}}.
@end defvar


@node Splash Screen Settings
@chapter Splash Screen Settings

The splash screen can be configured, in a rather limited way.

@c TEXI DOCSTRING MAGIC: proof-splash-time
@defvar proof-splash-time 
Minimum number of seconds to display splash screen for.@*
The splash screen may be displayed for a wee while longer than
this, depending on how long it takes the machine to initialise
Proof General.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-splash-contents
@defvar proof-splash-contents 
Evaluated to configure splash screen displayed when entering Proof General.@*
A list of the screen contents.  If an element is a string or an image
specifier, it is displayed centred on the window on its own line.
If it is nil, a new line is inserted.
@end defvar






@node Global Constants
@chapter Global Constants

The settings here are internal constants used by Proof General.
You don't need to configure these for your proof assistant
unless you want to modify or extend the defaults.

@c TEXI DOCSTRING MAGIC: proof-general-name
@defvar proof-general-name 
Proof General name used internally and in menu titles.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-general-home-page
@defopt proof-general-home-page 
Web address for Proof General.

The default value is @code{"https://proofgeneral.github.io"}.
@end defopt
@c TEXI DOCSTRING MAGIC: proof-universal-keys
@defvar proof-universal-keys 
List of key bindings made for all proof general buffers.@*
Elements of the list are tuples @samp{(k . f)}
where @samp{k} is a key binding (vector) and @samp{f} the designated function.
@end defvar



@node Handling Multiple Files
@chapter Handling Multiple Files
@cindex Multiple files

Large proof developments are typically spread across multiple files.
Many provers support such developments by keeping track of dependencies
and automatically processing scripts. Proof General supports this
mechanism. The user's point of view is considered in the user manual.
Here, we describe the more technical nitty gritty.  This is what you
need to know when you customise another proof assistant to work with
Proof General.

Documentation for the configuration settings mentioned here appears in
the previous sections, this section is intended to help explain the use
of those settings.

Proof General maintains a list @code{proof-included-files-list} of files
which it thinks have been processed by the proof assistant.  When a file
which is on this list is visited in Emacs, it will be coloured entirely
blue to indicate that it has been processed.  No editing of the file
will be allowed (unless @code{proof-strict-read-only} allows it).


@c TEXI DOCSTRING MAGIC: proof-included-files-list
@defvar proof-included-files-list 
List of files currently included in proof process.@*
This list contains files in canonical truename format
(see @samp{@code{file-truename}}).

Whenever a new file is being processed, it gets added to this list
via the @samp{@code{proof-shell-process-file}} configuration settings.
When the prover retracts a file, this list is resynchronised via the
@samp{@code{proof-shell-retract-files-regexp}} and @samp{@code{proof-shell-compute-new-files-list}}
configuration settings.

Only files which have been @strong{fully} processed should be included here.
Proof General itself will automatically add the filenames of a script
buffer which has been completely read when scripting is deactivated.
It will automatically remove the filename of a script buffer which
is completely unread when scripting is deactivated.

NB: Currently there is no generic provision for removing files which
are only partly read-in due to an error, so ideally the proof assistant
should only output a processed message when a file has been successfully
read.
@end defvar

The way that @code{proof-included-files-list} is maintained is the key
to multiple file management.  Ideally you should not set this
variable directly, but instead use (some of) the various
configuration settings that enable functionality inside Proof
General for managing @code{proof-included-files-list} (see below
if the configuration setting do not suffice).

@vindex proof-shell-process-file
@vindex proof-shell-retract-files-regexp
@vindex proof-shell-compute-new-files-list
@vindex proof-cannot-reopen-processed-files

There is a range of strategies for managing multiple files.  Ideally,
file dependencies should be managed by the proof assistant.  Proof
General will use the prover's low-level commands to process a whole file
and its requirements non-interactively, without going through script
management.  So that the user knows which files have been processed, the
proof assistant should issue messages which Proof General can recognize
(``file @code{foo} has been processed'') --- see
@code{proof-shell-process-file}.  When the user wants to edit a file
which has been processed, the file must be retracted (unlocked).  The
proof assistant should provide a command corresponding to this action,
which undoes a given file and all its dependencies.  As each file is
undone, a message should be issued which Proof General can recognize
(``file @code{foo} has been undone'') -- see
@code{proof-shell-retract-files-regexp}.  (The function
@code{proof-shell-compute-new-files-list} should be set to calculate the
new value for @code{proof-included-files-list} after a retract message
has been seen).


@c The key idea is that we leave it to the specific proof assistant to
@c worry about managing multiple files, as far as possible.  Whenever the
@c proof assistant processes or retracts a file it must clearly say so, so
@c that Proof General can register this.

As well as this communication from the assistant to Proof General about
processed or retracted files, Proof General can communicate the other
way: it will tell the proof assistant when it has processed or retracted
a file via script management.  This is because during script management,
the proof assistant may not be aware that it is actually dealing with a
file of proof commands (rather than just terminal input).

Proof General will provide this information in two special instances.
First, when scripting is turned off in a file that has been completely
processed, Proof General will tell the proof assistant using
@code{proof-shell-inform-file-processed-cmd}.  Second, when scripting is
turned on in a file which is completely processed, Proof General will
tell the proof assistant to reconsider: the file should not be
considered completely processed yet.  This uses the setting
@code{proof-shell-inform-file-retracted-cmd}.  This second, retracting,
case might lead to a series of messages from the prover telling Proof
General to unlock files which depend on the present one, again via
@code{proof-shell-retract-files-regexp}.  

The special case for retracting is the primary file the user wishes to
edit: this is automatically removed from
@code{proof-included-files-list}, but it depends on the proof assistant
whether or not it is possible to revert to a partially processed version
of the file (or "undo into" it).  This is the reason for the setting
@code{proof-cannot-reopen-processed-files}.  If this is non-nil, any
attempt to undo a fully processed file will unlock the entire file
(whether or not Proof General itself has history information for the
file).

What we have described so far is the ideal case, but it may require some
support from the proof assistant to set up (for example, if file-level
undo is not normally supported, or the messages during file processing
are not suitable).  Moreover, some proof assistants may not have file
handling with dependencies, or may have a particularly simple case of a
linear context: each file depends on all the ones processed before it.
Proof General allows you a shortcut to get automatic management of
multiple files in these cases by setting the flag
@code{proof-auto-multiple-files}.  This setting is probably an
approximation to the right thing for any proof assistant.  More files
than necessary will be retracted if the prover has a tree-like file
dependency rather than a linear one.

@vindex proof-shell-eager-annotation-start
@vindex proof-shell-eager-annotation-end
Finally, we should mention how Proof General recognizes file processing
messages from the proof assistant.  Proof General considers @var{output}
delimited by the the two regular expressions
@code{proof-shell-eager-annotation-start} and
@code{proof-shell-eager-annotation-end} as being important. It displays
the @var{output} in the Response buffer and analyses the contents
further. Among other important messages characterised by these regular
expressions (warnings, errors, or information), the prover can tell the
interface whenever it processes or retracts a file.


To summarize, the settings for multiple file management that may be
customized are as follows. To recognize file-processing,
@code{proof-shell-process-file}.  To recognize messages about file
undoing, @code{proof-shell-retract-files-regexp} and
@code{proof-shell-compute-new-files-list}.  @xref{Settings for matching
urgent messages from proof process}.  To tell the prover about files
handled with script management, use
 @code{proof-shell-inform-file-processed-cmd} and
 @code{proof-shell-inform-file-retracted-cmd}.  @xref{Proof shell commands}.
If your prover does not allow re-opening of closed
files, set @code{proof-cannot-reopen-processed-files} to @code{t}.
  Finally, set the flag @code{proof-auto-multiple-files} 
for a automatic approximation to multiple file handling.
@xref{Proof Script Settings}.

Internally Proof General uses
@code{proof-register-possibly-new-processed-file} to add a file
to @code{proof-included-files-list} and to possibly inform the
prover about this fact, @xref{Proof script mode}. The function
@code{proof-shell-process-urgent-message-retract} is responsible
for taking (possibly several) files off
@code{proof-included-files-list}. It relies on
@code{proof-shell-compute-new-files-list} (@pxref{Settings for
matching urgent messages from proof process}) to compute the new
value of @code{proof-included-files-list} and then calls
@code{proof-restart-buffers} on all those buffers that have been
taken off from @code{proof-included-files-list}, @xref{Proof
script mode}.


@node Configuring Editing Syntax
@chapter Configuring Editing Syntax
@cindex syntax table

Emacs has some standard settings which configure the syntax of major
modes.  The main setting is the @i{syntax table}, which determines the
syntax of programming elements such as strings, comments, and
parentheses.  To configure the syntax table, you can either write calls
to @code{modify-syntax-entry} in your mode functions, or set the
following variables to contain the tables for each mode.  (The main mode
to be concerned about is of course the proof script, where user editing
takes place).

@c TEXI DOCSTRING MAGIC: proof-script-syntax-table-entries
@defvar proof-script-syntax-table-entries 
List of syntax table entries for proof script mode.@*
A flat list of the form
@lisp
  (@var{char} @var{syncode} @var{char} @var{syncode} ...)
@end lisp
See doc of @samp{@code{modify-syntax-entry}} for details of characters
and syntax codes.

At present this is used only by the @samp{@code{proof-easy-config}} macro.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-syntax-table-entries 
@defvar proof-shell-syntax-table-entries 
List of syntax table entries for proof script mode.@*
A flat list of the form
@lisp
  (@var{char} @var{syncode} @var{char} @var{syncode} ...)
@end lisp
See doc of @samp{@code{modify-syntax-entry}} for details of characters
and syntax codes.

At present this is used only by the @samp{@code{proof-easy-config}} macro.
@end defvar
Some additional useful settings are:

@c magic by hand: comment-quote-nested
@defvar comment-quote-nested 
Non-nil if nested comments should be quoted.  
This should be locally set by each major mode if needed.  The
default setting is non-nil: modes which allow nested comments may set
this to nil.
@end defvar

@defvar outline-regexp
Regular expression to match the beginning of a heading.
Any line whose beginning matches this regexp is considered to start a heading.
@end defvar

@defvar outline-heading-end-regexp
Regular expression to match the beginning of a heading.
Any line whose beginning matches this regexp is considered to start a heading.
@end defvar

@node Configuring Font Lock
@chapter Configuring Font Lock
@cindex font lock

Support for Font Lock in Proof General is described in the user manual
(see the @i{Syntax highlighting} section).  To configure Font Lock for a
new proof assistant, you need to set the variable
@code{font-lock-keywords} in each of the mode functions you want
highlighting for.  Proof General will automatically install these
settings, and use font lock minor mode (for syntax highlighting as you
type) in script buffers.

@c nope: too big. TEXI DOCSTRING MAGIC: font-lock-keywords
To understand its format, check the documentation of
@code{font-lock-keywords} inside Emacs.

Instead of setting @code{font-lock-keywords} in each mode function, you
can use the following four variables to make the settings in place.
This is particularly useful if use the easy configuration mechanism for
Proof General, @pxref{Demonstration instance and easy configuration}.

@c TEXI DOCSTRING MAGIC: proof-script-font-lock-keywords
@defvar proof-script-font-lock-keywords 
Value of @samp{@code{font-lock-keywords}} used to fontify proof scripts.@*
The proof script mode should set this before calling @samp{@code{proof-config-done}}.
Used also by @samp{@code{proof-easy-config}} mechanism.
See also @samp{@code{proof-goals-font-lock-keywords}} and @samp{@code{proof-response-font-lock-keywords}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goals-font-lock-keywords
@defvar proof-goals-font-lock-keywords 
Value of @samp{@code{font-lock-keywords}} used to fontify the goals output.@*
The goals shell mode should set this before calling @samp{@code{proof-goals-config-done}}.
Used also by @samp{@code{proof-easy-config}} mechanism.
See also @samp{@code{proof-script-font-lock-keywords}} and @samp{@code{proof-response-font-lock-keywords}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-response-font-lock-keywords
@defvar proof-response-font-lock-keywords 
Value of @samp{@code{font-lock-keywords}} used to fontify the response output.@*
The response mode should set this before calling @samp{@code{proof-response-config-done}}.
Used also by @samp{@code{proof-easy-config}} mechanism.
See also @samp{@code{proof-script-font-lock-keywords}} and @samp{@code{proof-goals-font-lock-keywords}}.
@end defvar
Proof General provides a special function, @code{proof-zap-commas}, for
tweaking the font lock behaviour of provers which have declarations of
the form @code{x,y,z:Ty}.  This function removes highlighting on the
commas, and can be added as the last element of
@code{font-lock-keywords}.  Further manipulation of font lock behaviour
can be achieved via two hook functions which are run before and after
fontifying the output buffers.

@c TEXI DOCSTRING MAGIC: proof-zap-commas
@defun proof-zap-commas limit
Remove the face of all @samp{,} from point to @var{limit}.@*
Meant to be used from @samp{@code{font-lock-keywords}} as a way
to unfontify commas in declarations and definitions.
Useful for provers which have declarations of the form x,y,z:Ty
All that can be said for it is that the previous ways of doing
this were even more bogus....
@end defun

@c TEXI DOCSTRING MAGIC: pg-before-fontify-output-hook
@defvar pg-before-fontify-output-hook 
This hook is called before fontifying a region in an output buffer.@*
A function on this hook can alter the region of the buffer within
the current restriction, and must return the final value of (@code{point-max}).
[This hook is presently only used by phox-sym-lock].
@end defvar

@c TEXI DOCSTRING MAGIC: pg-after-fontify-output-hook
@defvar pg-after-fontify-output-hook 
This hook is called before fonfitying a region in an output buffer.@*
[This hook is presently only used by Isabelle].
@end defvar



@node Configuring Tokens
@chapter Configuring Tokens
@cindex Unicode Tokens
@cindex Tokens

Unicode Tokens is basically an overly complicated way of configuring
font-lock, along with some helpful menus.  The font lock configuration
makes use of recent Emacs features, particularly including
@code{compose-region} which allows the presentation of the buffer be
different from the underlying buffer contents.  Compared with the
X-Symbol package used previously by Proof General, this has the huge
advantage of not requiring the underlying text to be changed to display
symbols.  

Usage of the Unicode Tokens package is described in the Proof General
user manual, @pxref{Unicode symbols and special layout
support,,,ProofGeneral}.

@c FIXME TODO: add documentation here to explain config of Unicode Tokens

@c TEXI DOCSTRING MAGIC: proof-tokens-activate-command
@defvar proof-tokens-activate-command 
Command to activate token input/output for prover.@*
If non-nil, this command is sent to the proof assistant when
Unicode Tokens support is activated.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-tokens-deactivate-command
@defvar proof-tokens-deactivate-command 
Command to deactivate token input/output for prover.@*
If non-nil, this command is sent to the proof assistant when
Unicode Tokens support is deactivated.
@end defvar
We expect tokens to be used uniformly, so that along with each script
mode buffer, the response buffer and goals buffer also invoke Tokens
to display special characters in the same token language.  This happens
automatically.  If you want additional modes to use Tokens with the
token language for your proof assistant, you can set
@code{proof-tokens-extra-modes}.

@c TEXI DOCSTRING MAGIC: proof-tokens-extra-modes
@defvar proof-tokens-extra-modes 
List of additional mode names to use with Proof General tokens.@*
These modes will have Tokens enabled for the proof assistant token language,
in addition to the four modes for Proof General (script, shell, response, pbp).

Set this variable if you want additional modes to also display
tokens (for example, editing documentation or source code files).
@end defvar



@node Configuring Proof-Tree Visualization
@chapter Configuring Proof-Tree Visualization

@b{Parts of this section are outdated. Please create an issue at
github.com/ProofGeneral/Proof General if you have a question for
adapting Prooftree for a new proof assistant.}

The proof-tree visualization feature was written with the idea of
supporting Coq as well as other proof assistants. Nevertheless,
supporting proof-tree visualization for a second proof assistant
will almost certainly require changes in the generic Elisp code
in @code{generic/proof-tree.el} as well as in the
Prooftree program.

@menu
* A layered set of proof trees::
* Prerequisites::
* Proof-Tree Display Internals::
* Configuring Prooftree for a New Proof Assistant::
@end menu


@node A layered set of proof trees
@section A layered set of proof trees

Prooftree can actually display more than one proof tree per
proof. This is necessary to support the 
@code{Grab Existential Variables} command in Coq. When the main
goal has been proved, this command turns all open existential
variables into new proof obligations. All these new proof
obligations become root nodes for their own proof trees. When
they all have been proved one can again grab the open existential
variables...

For each proof, Prooftree can therefore display several layers,
where each layer can contain several (graphically) independent
proof trees. The first layer contains one tree for the original
proof goal. The second layer contains proof trees for goals that
have been added to the proof after the first proof tree was
completed. And so on.

Prooftree assumes a new layer when it receives new goals in a state
where the number of open goals is zero.


@node Prerequisites
@section Prerequisites

Proof-tree visualization requires certain support from the proof
assistant. Patching the proof assistant is therefore the first
step of adding support for proof-tree visualization. The
following features are needed.

@table @asis
@item Unique goal identification
The proof assistant must assign and output a unique string for
each goal. For Coq the internal @code{evar} index number is used,
which is printed for each goal in the form @code{(ID XXX)} when
Coq is started with the option @code{-emacs}.

The unique goal identification is needed to distinguish newly
spawned subgoals from older open subgoals and to mark the current
goal in the proof-tree display.

@item Indication of newly generated subgoals
A proof command that spawns additional subgoals must somehow
indicate the goal ID's of these new subgoals. Otherwise the
proof-tree display will not be able to reconstruct the proof-tree
structure. 

For Coq the newly spawned subgoals appear always in the list of
additional subgoals below the current goal. Note, that it is not
required to mark the newly spawned subgoals. They may appear in a
mixed list with older open subgoals. Note further, that it is not
required that always the complete set of all open subgoals is
printed (which is indeed not the case after of @code{Focus}
command in Coq). It is only required that the goal ID's of all
newly spawned subgoals is somehow printed.

@item State number for undo
There must be a state number that is strictly increasing when
asserting proof commands and that is reset to the appropriate
number after retracting some proof commands.

For Coq the state number in the extended prompt (visible only
with option @code{-emacs}) is used. 

@item Information about existential variables
Existential variables are placeholders that might or must be
instantiated later in the proof. Prooftree supports
existential variables with three features. Firstly, it can update
goals when existential variables get instantiated. Secondly, it
can mark the proof commands that introduced or instantiated
existential variables and, thirdly, it can display and track
dependencies between existential variables.

For the first feature, the proof assistant must list the currently
instantiated existential variables for every goal. For the second
feature it must additionally list the not instantiated
existential variables. Finally, for the third feature, it must
display the dependencies for instantiated existential variables.

For Coq, all necessary information is provided in the existential
evar line, that is printed with the @code{-emacs} switch.

@end table


@node Proof-Tree Display Internals
@section Proof-Tree Display Internals

This section gives some information about the inner structure of
the code that realizes the proof-tree display. The idea here is
that this section provides the background information to make the
documentation of the customizable variables of the proof-tree
Elisp code easy to understand.

@menu
* Organization of the Code::
* Communication::
* Guards::
* Urgent and Delayed Actions::
* Full Annotation::
@end menu


@node Organization of the Code
@subsection Organization of the Code

The proof-tree display is realized by Proof General in
cooperation with the external Prooftree program. The
latter is a GTK application in OCaml. Both, the Elisp code in
Proof General and the Prooftree OCaml code is divided into
a generic and a proof assistant specific part.

The generic Elisp code lives in @code{generic/proof-tree.el}. As
usual in Proof General, it contains various customizable
variables, which the proof assistant specific code must set. Most
of these variables contain regular expressions, but there are also
some that hold functions. The Coq specific code for the
proof-tree display is distributed in a few chunks over
@code{coq/coq.el}. 

The main task of the Elisp code is to extract goals, undo events
and information about existential variables from the
proof-assistant output and to send all this data to Prooftree.
Additional commands inserted by Prooftree are flagged with
@code{proof-tree-show-subgoal}, @code{no-goals-display} and
@code{no-response-display}. The flag
@code{proof-tree-show-subgoal} ensures that a number of internal
functions ignore these additional commands. The other two flags
ensure that their output is neither displayed in the goals nor
the response buffer.


In Prooftree the separation between generic and proof-assistant
specific code is less obvious. The Coq specific code is in the
file @code{coq.ml}. All the remaining code is generic. 

Prooftree opens for each proof a separate window. It reconstructs
the proof tree and orders the existential variables in a
dependency hierarchy. It stores a complete history of previous
states to support arbitrary undo operations. Under normal
circumstances one starts just one Prooftree process that keeps
running for the remainder of the Proof General session,
regardless of how many proof-tree windows are displayed.

A fair amount of the Prooftree code is documented with
@code{ocamldoc} documentation comments. With @code{make doc} they
can be converted into a set of html pages in the @code{doc}
subdirectory.


@node Communication
@subsection Communication

Prooftree is a standard Emacs subprocess that reads goals and
other proof status messages from its standard input. The
communication between Proof General and Prooftree is almost one
way only. Proof General sends proof status messages to Prooftree,
from which Prooftree reconstructs the current proof status and
the complete proof tree. Prooftree never requests additional
information from Proof General. 

There are only a few messages that Prooftree sends to Proof
General. These messages communicate user requests to Proof
General, for instance, when the user selects the undo menu item,
or when he closes the Prooftree window.

The communication protocol is completely described in the
@code{ocamldoc} documentation of @code{input.ml} in the Prooftree
sources. All messages consist of UTF-8 encoded human-readable
strings. The strings have either a fixed length or their byte-length
is encoded in the message before the string itself. 

For debugging purposes Prooftree can save all input in a file.
This feature can be turned on in the @code{Debug} tab of the
Prooftree configuration dialog or with option @code{-tee}. The
text that Prooftree sends to Proof General can be found in buffer
@code{*proof-tree*}.


@node Guards
@subsection Guards

The proof-tree display code inside Proof General uses two guard
variables. 

@c TEXI DOCSTRING MAGIC: proof-tree-configured
@defvar proof-tree-configured 
Whether external proof-tree display is configured.@*
This boolean enables the proof-tree menu entry and the function
that starts external proof-tree display.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-tree-external-display
@defvar proof-tree-external-display 
Display proof trees in external prooftree windows if t.@*
Actually, if this variable is t then the user requested an
external proof-tree display.  If there was no unfinished proof
when proof-tree display was requested and if no proof has been
started since then, then there is obviously no proof-tree
display.  In this case, this variable stays t and the proof-tree
display will be started for the next proof.

Controlled by @samp{@code{proof-tree-external-display-toggle}}.
@end defvar

In Proof General, the code for the external proof-tree display is
called from the proof-shell filter function in
@code{proof-shell-exec-loop} and
@code{proof-shell-filter-manage-output}, @pxref{Proof shell
mode}. The variable @code{proof-tree-external-display} is a guard
for these calls, to ensure that the proof-tree specific code is
only called if the user requested a proof-tree display.

The whole proof-tree package contains only one function that can
be called interactively:
@code{proof-tree-external-display-toggle}, which switches
@code{proof-tree-external-display} on and off. When
@code{proof-tree-configured} is @code{nil},
@code{proof-tree-external-display-toggle} aborts with an error
message. 

@c TEXI DOCSTRING MAGIC: proof-tree-external-display-toggle
@deffn Command proof-tree-external-display-toggle 
Toggle the external proof-tree display.@*
When called outside a proof the external proof-tree display will
be enabled for the next proof.  When called inside a proof the
proof display will be created for the current proof.  If the
external proof-tree display is currently on, then this toggle
will switch it off.  At the end of the proof the proof-tree
display is switched off.
@end deffn


@node Urgent and Delayed Actions
@subsection Urgent and Delayed Actions

The proof-shell filter functions contains two calls to proof-tree
specific code. One for urgent actions and one for all remaining
actions, that can be delayed.

Urgent actions are those that must be executed before
@code{proof-shell-exec-loop} sends the next item from
@code{proof-action-list} to the proof assistant. For execution
speed, the amount of urgent code should be kept small.

@c TEXI DOCSTRING MAGIC: proof-tree-check-proof-finish
@defun proof-tree-check-proof-finish last-item
Urgent action to delay processing at proof end.@*
This function is called from @samp{@code{proof-shell-exec-loop}} after the
old item has been removed and before the next item from
@samp{@code{proof-action-list}} is sent to the proof assistant. Of course
only when the proof-tree display is active. At the end of the
proof, this function delays items just following the previous
proof until all show-goal commands from prooftree and the
@samp{@code{proof-tree-display-stop-command}} (which switches the dependent
evar line off for Coq) have been processed.

If this function detects the end of the proof, it moves
non-priority items following in @samp{@code{proof-action-list}} to
@samp{@code{proof-tree--delayed-actions}} and sets
@samp{@code{proof-second-action-list-active}}. When later the command from
@samp{@code{proof-tree-display-stop-command}} is recognized, the items are
moved back. If no items follow the end of the previous proof,
@samp{@code{proof-tree-display-stop-command}} is set to t.
@end defun


The function @code{proof-tree-check-proof-finish} is called at a point
where it is save to manipulate @code{proof-action-list}. This is
essential, because @code{proof-tree-urgent-action} inserts goal
display commands into @code{proof-action-list} when existential
variables got instantiated and when the sequent text from newly
created subgoals is missing.


Most of the proof-tree specific code runs when the proof
assistant is already busy with the next item from
@code{proof-action-list}. 

@c TEXI DOCSTRING MAGIC: proof-tree-handle-delayed-output
@defun proof-tree-handle-delayed-output old-proof-marker cmd flags _span
Process delayed output for prooftree.@*
This function is the main entry point of the Proof General
prooftree support.  It examines the delayed output in order to
take appropriate actions and maintains the internal state.

The delayed output to handle is in the region
[@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}].
Urgent messages might be before that, following @var{old-proof-marker},
which contains the position of @samp{@code{proof-marker}}, before the next
command was sent to the proof assistant.

All other arguments are (former) fields of the @samp{@code{proof-action-list}}
entry that is now finally retired.  @var{cmd} is the command, @var{flags} are
the flags and @var{span} is the span.
@end defun

The function @code{proof-tree-handle-delayed-output} does all the
communication with Prooftree. 


@node Full Annotation
@subsection Full Annotation

In the default configuration Proof General switches the proof
assistant into quiet mode if there are more than
@code{proof-shell-silent-threshold} items in
@code{proof-action-list}, see Section @i{Document centred
working} (in Chapter @i{Advanced Script Management and Editing})
in the @i{Proof General} users manual. The proof-tree display
needs of course the full output from the proof assistant.
Therefore @code{proof-shell-should-be-silent} keeps the proof
assistant noisy when the proof-tree display is switched on.


@node Configuring Prooftree for a New Proof Assistant
@section Configuring Prooftree for a New Proof Assistant

To get the proof-tree display running for a new proof assistant
one has to configure the proof-tree Elisp code and adapt the
Prooftree program.

@menu
* Proof Tree Elisp configuration::
* Prooftree Adaption::
@end menu

@node Proof Tree Elisp configuration
@subsection Proof Tree Elisp configuration

All variables that need to be configured are in the customization
group @code{proof-tree-internals}. Most of these variables are
regular expressions for extracting various parts from the proof
assistant output. However, some are functions that need to be
implemented as prover specific part of the proof display code.

The variables @code{proof-tree-configured},
@code{proof-tree-get-proof-info} and
@code{proof-tree-find-begin-of-unfinished-proof} might be used
before the proof assistant is running inside a proof shell. They
must therefore be configured as part of the proof assistant
editing mode. 

The other variables are only used when the proof shell is
running. They can therefore be configured with the
proof assistant proof-shell mode.


@node Prooftree Adaption
@subsection Prooftree Adaption

To make the new proof assistant known to Prooftree, the match in
function @code{configure_prooftree} in @code{input.ml} must be
extended. If the new proof assistant does not support existential
variables adding a line
@example
  | "new-pa-name" -> ()
@end example
suffices.

If the new prover supports existential variables, Prooftree must
be extended with a parser for the existential variable
information printout of the proof assistant. The parser for Coq
is contained in the file @code{coq.ml}. Then the function
@code{configure_prooftree} must assign this new parser to the
reference @code{parse_existential_info}.


@node Writing More Lisp Code
@chapter Writing More Lisp Code

You may want to add some extra features to your instance of Proof
General which are not supported in the generic core.  To do this, you
can use the settings described above, plus a small number of fundamental
functions in Proof General which you can consider as exported in the
generic interface.  Be careful using more functions than are mentioned
here because the internals of Proof General may change between versions.

@menu
* Default values for generic settings::
* Adding prover-specific configurations::
* Useful variables::
* Useful functions and macros::        
@end menu

@node Default values for generic settings
@section Default values for generic settings

Several generic settings are defined using @code{defpgcustom} in
@file{proof-config.el}.  This introduces settings of the form
@code{<PA>-name} for each proof assistant @var{PA}.

To set the default value for these settings in prover-specific cases,
you should use the special @code{defpgdefault} macro:

@c TEXI DOCSTRING MAGIC: defpgdefault
@deffn Macro defpgdefault 
Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@*
This should be used in prover-specific code to alter the default values
for prover specific settings.

Usage: (defpgdefault SYM @var{value})
@end deffn

In your prover-specific code you can simply use the setting
@code{<PA>-sym} directly, i.e., write @code{myprover-home-page}.

In the generic code, you can use a macro, writing @code{(proof-ass
home-page)} to refer to the @code{<PA>-home-page} setting for the
currently running instance of Proof General.

@xref{Configuration variable mechanisms}, for more details on this
mechanism.


@node Adding prover-specific configurations
@section Adding prover-specific configurations

Apart from the generic settings, your prover instance will probably need
some specific customizable settings.

Defining new prover-specific settings using customize is pretty easy.
You should do it at least for your prover-specific user options.

The code in @file{proof-site.el} provides each prover with two
customization groups automatically (based on the name of the assistant): 
@code{<PA>} for user options for prover @var{PA}
and 
@code{<PA>-config} for configuration of prover @var{PA}.
Typically @code{<PA>-config} holds settings which are
constants but which may be nice to tweak.

The first group appears in the menu
@lisp
  ProofGeneral -> Advanced -> Customize -> <PA> 
@end lisp
The second group appears in the menu:
@lisp
  ProofGeneral -> Internals -> <PA> config
@end lisp

A typical use of @code{defcustom} looks like this:
@lisp
(defcustom myprover-search-page
  "http://findtheorem.myprover.org"
  "URL of search web page for myprover."
  :type 'string
  :group 'myprover-config)
@end lisp
This introduces a new customizable setting, which you might use to make
a menu entry, for example.  The default value is the string
@code{"http://findtheorem.myprover.org"}.






@node Useful variables
@section Useful variables

In @file{proof-site}, some architecture flags are defined.  These
can be used to write conditional pieces of code for different Emacs
and operating systems.  They are referred to mainly in
@file{proof-compat} (which helps to keep the architecture and version
dependent code in one place).


@node Useful functions and macros
@section Useful functions and macros

The recommended functions you may invoke are these:

@itemize @bullet
@item Any of the interactive commands (i.e. anything you
 can invoke with @kbd{M-x}, including all key-bindings)
@item Any of the internal functions and macros mentioned below
@end itemize

To insert text into the current (usually script) buffer, the function
@code{proof-insert} is useful.  There's also a handy macro
@code{proof-defshortcut} for defining shortcut functions using it.


@c TEXI DOCSTRING MAGIC: proof-insert
@defun proof-insert text
Insert @var{text} into the current buffer.@*
@var{text} may include these special characters:
@lisp
  %p  - place the point here after input
@end lisp
Any other %-prefixed character inserts itself.
@end defun

@c TEXI DOCSTRING MAGIC: proof-defshortcut
@deffn Macro proof-defshortcut 
Define shortcut function FN to insert @var{string}, optional keydef KEY.@*
This is intended for defining proof assistant specific functions.
@var{string} is inserted using @samp{@code{proof-insert}}, which see.
KEY is added onto proof assistant map.
@end deffn
The function @code{proof-shell-invisible-command} is a useful utility
for sending a single command to the process.  You should use this to
implement user-level or internal functions rather than attempting to
directly manipulate the proof action list, or insert into the shell
buffer.

@c TEXI DOCSTRING MAGIC: proof-shell-invisible-command
@defun proof-shell-invisible-command cmd &optional wait invisiblecallback &rest flags
Send @var{cmd} to the proof process.@*
The @var{cmd} is @samp{invisible} in the sense that it is not recorded in buffer.
@var{cmd} may be a string or a string-yielding expression.

Automatically add @samp{@code{proof-terminal-string}} if necessary, examining
@samp{proof-shell-no-auto-terminate-commands}.

By default, let the command be processed asynchronously.
But if optional @var{wait} command is non-nil, wait for processing to finish
before and after sending the command.

In case @var{cmd} is (or yields) nil, do nothing.

@var{invisiblecallback} will be invoked after the command has finished,
if it is set.  It should probably run the hook variables
@samp{@code{proof-state-change-hook}}.

@var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}.
The flag @code{'invisible} is always added to @var{flags}.
@end defun

There are several handy macros to help you define functions
which invoke @code{proof-shell-invisible-command}.

@c TEXI DOCSTRING MAGIC: proof-definvisible
@deffn Macro proof-definvisible 
Define function FN to send @var{string} to proof assistant, optional keydef KEY.@*
This is intended for defining proof assistant specific functions.
@var{string} is sent using @samp{@code{proof-shell-invisible-command}}, which see.
@var{string} may be a string or a function which returns a string.
KEY is added onto proof assistant map.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-define-assistant-command
@deffn Macro proof-define-assistant-command 
Define FN (docstring DOC): check if @var{cmdvar} is set, then send @var{body} to prover.@*
@var{body} defaults to @var{cmdvar}, a variable.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg
@deffn Macro proof-define-assistant-command-witharg 
Define FN (arg) with DOC: check @var{cmdvar} is set, @var{prompt} a string and eval @var{body}.@*
The @var{body} can contain occurrences of arg.
@var{cmdvar} is a variable holding a function or string.  Automatically has history.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-format-filename
@defun proof-format-filename string filename
Format @var{string} by replacing quoted chars by escaped version of @var{filename}.

%e uses the canonicalized expanded version of filename (including
directory, using @samp{@code{default-directory}} -- see @samp{@code{expand-file-name}}).

%r uses the unadjusted (possibly relative) version of @var{filename}.

%m ('module') uses the basename of the file, without directory
or extension.

%s means the same as %e.

Using %e can avoid problems with dumb proof assistants who don't
understand ~, for example.

For all these cases, the escapes in @samp{@code{proof-shell-filename-escapes}}
are processed.

If @var{string} is in fact a function, instead invoke it on @var{filename} and
return the resulting (string) value.
@end defun

@node Internals of Proof General
@chapter Internals of Proof General

This chapter sketches some of the internal functions and variables of
Proof General, to help developers who wish to understand or modify the
code.

Most of the documentation below is generated automatically from the
comments in the code.  Because Emacs lisp is interpreted and
self-documenting, the best way to find your way around the source is
inside Emacs once Proof General is loaded.  Read the source files, and
use functions such as @kbd{C-h v} and @kbd{C-h f}.

The code is split into files.  The following sections document the
important files, kept in the @file{generic/} subdirectory.

@menu
* Spans::                       
* Proof General site configuration::  
* Configuration variable mechanisms::
* Global variables::            
* Proof script mode::           
* Proof shell mode::
* Debugging::
@end menu


@c
@c SECTION: Global variables
@c
@node Spans
@section Spans
@cindex spans
@cindex extents
@cindex overlays

@dfn{Spans} are an abstraction of Emacs @dfn{overlays} originally used
to help bridge the gulf between GNU Emacs and XEmacs. See the file
@file{lib/span.el}. XEmacs calls these @dfn{extents} which is a name
still used in some parts of the code.


@c
@c SECTION: Proof General site configuration
@c
@node Proof General site configuration
@section Proof General site configuration
@cindex installation directories
@cindex site configuration

The file @file{proof-site.el} contains the initial configuration for
Proof General for the site (or user) and the choice of provers.

The first part of the configuration is to set
@code{proof-home-directory} to the directory that @file{proof-site.el}
is located in, or to the variable of the environment variable
@code{PROOFGENERAL_HOME} if that is set.

@c TEXI DOCSTRING MAGIC: proof-home-directory
@defvar proof-home-directory 
Directory where Proof General is installed.@*
Based on where the file @samp{proof-site.el} was loaded from.
Falls back to consulting the environment variable @samp{PROOFGENERAL_HOME} if
proof-site.el couldn't know where it was executed from.
@end defvar

@c They're no longer options.
@c The default value for @code{proof-home-directory} mentioned above is the
@c one for the author's system, it won't be the same for you!

Further directory variables allow the files of Proof General to be split
up and installed across a system if need be, rather than under the
@code{proof-home-directory} root.

@c TEXI DOCSTRING MAGIC: proof-images-directory
@defvar proof-images-directory 
Where Proof General image files are installed.  Ends with slash.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-info-directory
@defvar proof-info-directory 
Where Proof General Info files are installed.  Ends with slash.
@end defvar



@cindex mode stub
After defining these settings, we define a @dfn{mode stub} for each
proof assistant enabled.  The mode stub will autoload Proof General for
the right proof assistant when a file is visited with the corresponding
extension.  The proof assistants enabled are the ones listed
in the @code{proof-assistants} setting.

@c TEXI DOCSTRING MAGIC: proof-assistants
@defvar proof-assistants 
Choice of proof assistants to use with Proof General.@*
A list of symbols chosen from: @samp{coq} @samp{easycrypt} @samp{phox} @samp{qrhl} @samp{pgshell} @samp{pgocaml} @samp{pghaskell}.
If nil, the default will be ALL available proof assistants.

Each proof assistant defines its own instance of Proof General,
providing session control, script management, etc.  Proof General
will be started automatically for the assistants chosen here.
To avoid accidently invoking a proof assistant you don't have,
only select the proof assistants you (or your site) may need.

You can select which proof assistants you want by setting this
variable before @samp{proof-site.el} is loaded, or by setting
the environment variable @samp{PROOFGENERAL_ASSISTANTS} to the
symbols you want, for example "coq easycrypt".  Or you can
edit the file @samp{proof-site.el} itself.

Note: to change proof assistant, you must start a new Emacs session.
@end defvar

The file @file{proof-site.el} also defines a version variable.

@c TEXI DOCSTRING MAGIC: proof-general-version
@defvar proof-general-version 
Version string identifying Proof General release.
@end defvar



@c
@c SECTION: Configuration variable mechanisms
@c
@node Configuration variable mechanisms
@section Configuration variable mechanisms
@cindex conventions
@cindex user options
@cindex configuration
@cindex settings

The file @file{proof-config.el} defines the configuration variables for
Proof General, including instantiation parameters and user options.  See
previous chapters for details of its contents.  Here we mention some
conventions for declaring user options.

Global user options and instantiation parameters are declared using
@code{defcustom} as usual.  User options should have `@code{*}' as the
first character of their docstrings (standard Emacs convention) and live
in the customize group @code{proof-user-options}.  See
@file{proof-config.el} for the groups for instantiation parameters.

User options which are generic (having separate instances for each
prover) and instantiation parameters (by definition generic) can be
declared using the special macro @code{defpgcustom}.  It is used in the
same way as @code{defcustom}, except that the symbol declared will
automatically be prefixed by the current proof assistant symbol.

@c TEXI DOCSTRING MAGIC: defpgcustom
@deffn Macro defpgcustom 
Define a new customization variable <PA>@var{-sym} for the current proof assistant.@*
This is intended for defining settings which are useful for any prover,
but which the user may require different values of across provers.

The function proof-assistant-<SYM> is also defined, which can be used in the
generic portion of Proof General to access the value for the current prover.

Arguments @var{args} are as for @samp{defcustom}, which see.  If a :group argument is
not supplied, the setting will be added to the internal settings for the
current prover (named <PA>-config).
@end deffn

In specific instances of Proof General, the macro @code{defpgdefault}
can be used to give a default value for a generic setting.

@c TEXI DOCSTRING MAGIC: defpgdefault
@deffn Macro defpgdefault 
Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@*
This should be used in prover-specific code to alter the default values
for prover specific settings.

Usage: (defpgdefault SYM @var{value})
@end deffn

All new instantiation variables are best declared using the
@code{defpgcustom} mechanism (old code may be converted gradually).
Customizations which are liable to be different for different instances
of Proof General are also best declared in this way.  An example is the
use of X Symbol, controlled by @code{@emph{PA}-x-symbol-enable}, since
it works poorly or not at all with some provers.

To access the generic settings, the following four functions and
macros are useful.

@c TEXI DOCSTRING MAGIC: proof-ass
@deffn Macro proof-ass 
Return the value for SYM for the current prover.@*
This macro should only be invoked once a specific prover is engaged.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-ass-sym
@deffn Macro proof-ass-sym 
Return the symbol for SYM for the current prover.  SYM not evaluated.@*
This macro should only be called once a specific prover is known.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-ass-symv
@deffn Macro proof-ass-symv 
Return the symbol for SYM for the current prover.  SYM evaluated.@*
This macro should only be invoked once a specific prover is engaged.
@end deffn

If changing a user option setting amounts to more than just setting a
variable (it may have some dynamic effect), we can set the
@code{custom-set} property for the variable to the function
@code{proof-set-value} which does an ordinary @code{set-default} to set
the variable, and then calls a function with the same name as the
variable, to do whatever is necessary according to the new value for the
variable.  

There are several settings which can be switched on or off by the user,
which use this @code{proof-set-value} mechanism.  They are controlled by
boolean variables with names like @code{proof-@var{foo}-enable}, and
appear at the start of the customize group @code{proof-user-options}.
They should be edited by the user through the customization mechanism,
and set in the code using @code{customize-set-variable}.

In @code{proof-utils.el} there is a handy macro,
@code{proof-deftoggle}, which constructs an interactive function
for toggling boolean customize settings.  We can use this to make an
interactive function @code{proof-@var{foo}-toggle} to put on a menu or
bind to a key, for example.

This general scheme is followed as far as possible, to give uniform
behaviour and appearance for boolean user options, as well as
interfacing properly with the @code{customize} mechanism.

@c TEXI DOCSTRING MAGIC: proof-set-value
@defun proof-set-value sym value
Set a customize variable using @samp{@code{set-default}} and a function.@*
We first call @samp{@code{set-default}} to set @var{sym} to @var{value}.
Then if there is a function @var{sym} (i.e. with the same name as the
variable @var{sym}), it is called to take some dynamic action for the new
setting.

If there is no function @var{sym}, we try stripping
@samp{@code{proof-assistant-symbol}} and adding "proof-" instead to get
a function name.  This extends @code{proof-set-value} to work with
generic individual settings.

The dynamic action call only happens when values @strong{change}: as an
approximation we test whether proof-config is fully-loaded yet.
@end defun

@c TEXI DOCSTRING MAGIC: proof-deftoggle
@deffn Macro proof-deftoggle 
Define a function VAR-toggle for toggling a boolean customize setting VAR.@*
The toggle function uses @samp{@code{customize-set-variable}} to change the variable.
@var{othername} gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned.
@end deffn


@c
@c SECTION: Global variables
@c
@node Global variables
@section Global variables
@cindex variables


Global variables are defined in @file{proof.el}.  The same file defines
a few utility functions and some triggers to load in the other files.

@c TEXI DOCSTRING MAGIC: proof-script-buffer
@defvar proof-script-buffer 
The currently active scripting buffer or nil if none.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-buffer
@defvar proof-shell-buffer 
Process buffer where the proof assistant is run.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-response-buffer
@defvar proof-response-buffer 
The response buffer.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-goals-buffer
@defvar proof-goals-buffer 
The goals buffer.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-buffer-type
@defvar proof-buffer-type 
Symbol for the type of this buffer: @code{'script}, @code{'shell}, @code{'goals}, or @code{'response}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-included-files-list
@defvar proof-included-files-list 
List of files currently included in proof process.@*
This list contains files in canonical truename format
(see @samp{@code{file-truename}}).

Whenever a new file is being processed, it gets added to this list
via the @samp{@code{proof-shell-process-file}} configuration settings.
When the prover retracts a file, this list is resynchronised via the
@samp{@code{proof-shell-retract-files-regexp}} and @samp{@code{proof-shell-compute-new-files-list}}
configuration settings.

Only files which have been @strong{fully} processed should be included here.
Proof General itself will automatically add the filenames of a script
buffer which has been completely read when scripting is deactivated.
It will automatically remove the filename of a script buffer which
is completely unread when scripting is deactivated.

NB: Currently there is no generic provision for removing files which
are only partly read-in due to an error, so ideally the proof assistant
should only output a processed message when a file has been successfully
read.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed
@defvar proof-shell-proof-completed 
Flag indicating that a completed proof has just been observed.@*
If non-nil, the value counts the commands from the last command
of the proof (starting from 1).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen
@defvar proof-shell-error-or-interrupt-seen 
Flag indicating that an error or interrupt has just occurred.@*
Set to @code{'error} or @code{'interrupt} if one was observed from the proof
assistant during the last group of commands.
@end defvar


@c
@c SECTION: Proof script mode
@c
@node Proof script mode
@section Proof script mode

The file @file{proof-script.el} contains the main code for proof script
mode, as well as definitions of menus, key-bindings, and user-level
functions.

Proof scripts have two important variables for the locked and queue
regions.  These variables are local to each script buffer (although we
only really need one queue span in total rather than one per buffer).

@c TEXI DOCSTRING MAGIC: proof-locked-span
@defvar proof-locked-span 
The locked span of the buffer.@*
Each script buffer has its own locked span, which may be detached
from the buffer.
Proof General allows buffers in other modes also to be locked;
these also have a non-nil value for this variable.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-queue-span
@defvar proof-queue-span 
The queue span of the buffer.  May be detached if inactive or empty.@*
Each script buffer has its own queue span, although only the active
scripting buffer may have an active queue span.
@end defvar

Various utility functions manipulate and examine the spans.  An
important one is @code{proof-init-segmentation}.

@c TEXI DOCSTRING MAGIC: proof-init-segmentation
@defun proof-init-segmentation 
Initialise the queue and locked spans in a proof script buffer.@*
Allocate spans if need be.  The spans are detached from the
buffer, so the regions are made empty by this function.
Also clear list of script portions.
@end defun

For locking files loaded by a proof assistant, we use the next function.

@c TEXI DOCSTRING MAGIC: proof-complete-buffer-atomic
@defun proof-complete-buffer-atomic buffer
Ensure @var{buffer} marked completely processed, completing with a single step.

If buffer already contains a locked region, only the remainder of the
buffer is closed off atomically (although undo for the initial portion
is unlikely to work, the decoration may be worth retaining).

This works for buffers which are not in proof scripting mode too,
to allow other files loaded by proof assistants to be marked read-only.
@end defun

Atomic locking is instigated by the next function, which uses the
variables @code{proof-included-files-list} documented earlier
(@pxref{Handling Multiple Files} and @pxref{Global variables}).

@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file
@defun proof-register-possibly-new-processed-file file &optional informprover noquestions
Register a possibly new @var{file} as having been processed by the prover.

If @var{informprover} is non-nil, the proof assistant will be told about this,
to co-ordinate with its internal file-management.  (Otherwise we assume
that it is a message from the proof assistant which triggers this call).
In this case, the user will be queried to save some buffers, unless
@var{noquestions} is non-nil.

No action is taken if the file is already registered.

A warning message is issued if the register request came from the
proof assistant and Emacs has a modified buffer visiting the file.
@end defun

(Unlocking is done by
@code{proof-shell-process-urgent-message-retract} together with
@code{proof-restart-buffers}.)

An important pair of functions activate and deactivate scripting for the
current buffer.  A change in the state of active scripting can trigger
various actions, such as starting up the proof assistant, or altering
@code{proof-included-files-list}.

@c TEXI DOCSTRING MAGIC: proof-activate-scripting
@deffn Command proof-activate-scripting &optional nosaves queuemode
Ready prover and activate scripting for the current script buffer.

The current buffer is prepared for scripting.  No changes are
necessary if it is already in Scripting minor mode.  Otherwise, it
will become the new active scripting buffer, provided scripting can be
switched off in the previous active scripting buffer with
@samp{@code{proof-deactivate-scripting}}.

Activating a new script buffer is a good time to ask if the user
wants to save some buffers; this is done if the user option
@samp{@code{proof-query-file-save-when-activating-scripting}} is set and
provided the optional argument @var{nosaves} is non-nil.

The optional argument @var{queuemode} relaxes the test for a busy proof
shell to allow one which has mode @var{queuemode}.  In all other cases,
a proof shell busy error is given.

Finally, the hooks @samp{@code{proof-activate-scripting-hook}} are run.  This can
be a useful place to configure the proof assistant for scripting in a
particular file, for example, loading the correct theory, or whatever.
If the hooks issue commands to the proof assistant (via
@samp{@code{proof-shell-invisible-command}}) which result in an error, the
activation is considered to have failed and an error is given.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-deactivate-scripting
@deffn Command proof-deactivate-scripting &optional forcedaction
Try to deactivate scripting for the active scripting buffer.

Aims to set @samp{@code{proof-script-buffer}} to nil and turn off the
modeline indicator.  No action is required there is no active
scripting buffer.

We make sure that the active scripting buffer either has no locked
region or a full locked region (everything in it has been processed).
If this is not already the case, we question the user whether to
retract or assert, or automatically take the action indicated in the
user option @samp{@code{proof-auto-action-when-deactivating-scripting}}.

If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice
to fully retract the active scripting buffer.  In this case the
active scripting buffer is retracted even if it was fully processed.
Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process}
is ignored in this case.

If the scripting buffer is (or has become) fully processed, and it is
associated with a file, it is registered on
@samp{@code{proof-included-files-list}}.  Conversely, if it is (or has become)
empty, we make sure that it is @strong{not} registered.  This is to be
certain that the included files list behaves as we might expect with
respect to the active scripting buffer, in an attempt to harmonize
mixed scripting and file reading in the prover.

This function either succeeds, fails because the user refused to
process or retract a partly finished buffer, or gives an error message
because retraction or processing failed.  If this function succeeds,
then @samp{@code{proof-script-buffer}} is nil afterwards.

The optional argument @var{forcedaction} overrides the user option
@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents
questioning the user.  It is used to make a value for
the @samp{@code{kill-buffer-hook}} for scripting buffers, so that when
a scripting buffer is killed it is always retracted.
@end deffn

The function @code{proof-segment-up-to} is the main one used for parsing
the proof script buffer.  There are several variants of this function
available corresponding to different parsing strategies; the appropriate
one is aliased to @code{proof-segment-up-to} according to which
configuration variables have been set.  
@itemize @bullet
@item If @code{proof-script-sexp-commands} is set, the choice is 
 @code{proof-script-generic-parse-sexp}.
@ item If only @code{proof-script-command-end-regexp} or @code{proof-terminal-string} are set,
 then the default is @code{proof-script-generic-parse-cmdend}.
@item If @code{proof-script-command-start-regexp} is set, the choice is
 @code{proof-script-generic-parse-cmdstart}.  
@end itemize
The function @code{proof-semis-to-vanillas} uses
@code{proof-segment-up-to} to convert a parsed region of the script into
a series of commands to be sent to the proof assistant.

@c TEXI DOCSTRING MAGIC: proof-script-generic-parse-cmdend
@defun proof-script-generic-parse-cmdend 
For @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-command-end-regexp}} set.
@end defun

@c TEXI DOCSTRING MAGIC: proof-script-generic-parse-cmdstart
@defun proof-script-generic-parse-cmdstart 
For @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-command-start-regexp}} is set.
@end defun

@c TEXI DOCSTRING MAGIC: proof-script-generic-parse-sexp
@defun proof-script-generic-parse-sexp 
Used for @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-sexp-commands}} is set.
@end defun
@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas
@defun proof-semis-to-vanillas semis &optional queueflags
Create vanilla spans for @var{semis} and a list for the queue.@*
Proof terminator positions @var{semis} has the form returned by
the function @samp{proof-segment-up-to}.  The argument list is destroyed.
The callback in each queue element is @samp{@code{proof-done-advancing}}.

If the variable @samp{@code{proof-script-preprocess}} is set (to the name of
a function), call that function to construct the first element of
each queue item.

The optional @var{queueflags} are added to each queue item.
@end defun

The function @code{proof-assert-until-point} is the main one used to
process commands in the script buffer.  It's actually used to implement
the assert-until-point, electric terminator keypress, and
find-next-terminator behaviours.  In different cases we want different
things, but usually the information (i.e. are we inside a comment) isn't
available until we've actually run @code{proof-segment-up-to (point)},
hence all the different options when we've done so.

@c TEXI DOCSTRING MAGIC: proof-assert-until-point
@defun proof-assert-until-point &optional displayflags
Process the region from the end of the locked-region until point.
@end defun

The main command for retracting parts of a script is
@code{proof-retract-until-point}.

@c TEXI DOCSTRING MAGIC: proof-retract-until-point
@defun proof-retract-until-point &optional undo-action displayflags
Set up the proof process for retracting until point.@*
This calculates the commands to undo to the current point within
the locked region.  If invoked outside the locked region, undo
the last successfully processed command.  See @samp{@code{proof-retract-target}}.

After retraction has succeeded in the prover, the filter will call
@samp{@code{proof-done-retracting}}.  If @var{undo-action} is non-nil, it will
then be invoked on the region in the proof script corresponding to
the proof command sequence.
@var{displayflags} control output shown to user, see @samp{@code{proof-action-list}}.

Before the retraction is calculated, we enforce the file-level
protocol with @samp{@code{proof-activate-scripting}}.  This has a couple
of effects:

1. If the file is completely processed, we have to re-open it
for scripting again which may involve retracting
other (dependent) files.

2. We may query the user whether to save some buffers.

Step 2 may seem odd -- we're undoing (in) the buffer, after all
-- but what may happen is that when scripting starts going
forward again, we hit a command that loads other files, but the
user hasn't saved the latest edits.  Therefore it is right to
query saves here.
@end defun

To clean up when scripting is stopped, a script buffer is killed,
a file is retract (and thus must be unlocked), or the
proof assistant exits, we use the functions
@code{proof-restart-buffers} and
@code{proof-script-remove-all-spans-and-deactivate}.

@c TEXI DOCSTRING MAGIC: proof-restart-buffers
@defun proof-restart-buffers buffers
Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@*
The high-level effect is that all members of @var{buffers} are
completely unlocked, including all the necessary cleanup.  No
effect on a buffer which is nil or killed.  If one of the buffers
is the current scripting buffer, then @samp{@code{proof-script-buffer}} will
deactivated.
@end defun

@c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate
@defun proof-script-remove-all-spans-and-deactivate 
Remove all spans from scripting buffers via @samp{@code{proof-restart-buffers}}.
@end defun


@c
@c SECTION: Proof Shell Mode
@c
@node Proof shell mode
@section Proof shell mode
@cindex proof shell mode
@cindex comint-mode
@cindex scomint-mode

The proof shell mode code is in the file @file{proof-shell.el}.  Proof
shell mode is defined to inherit from @code{scomint-mode} using
@code{define-derived-mode} near the end of the file.  The
@file{scomint.el} package stands for ``simplified comint'', where
@code{comint-mode} is the standard Emacs mode for running an
embedded command interpreter.  In @code{scomint}, many of the
interactive commands have been removed to speed up the process
handling, because it isn't intended that the user interacts
directly with the shell in Proof General.

The bulk of the code in the @code{proof-shell} package is concerned with
sending code to and from the shell, and processing output for the
associated buffers (goals and response).

Good process handling is a tricky issue.  Proof General attempts to
manage the process strictly, by maintaining a queue of commands to send
to the process.  Once a command has been processed, another one is
popped off the queue and sent.

There are several important internal variables which control
interaction with the process.

@c TEXI DOCSTRING MAGIC: proof-shell-busy
@defvar proof-shell-busy 
A lock indicating that the proof shell is processing.

The lock notes that we are processing a queue of commands being
sent to the prover, and indicates whether the commands correspond
to script management from a buffer (rather than being ad-hoc
query commands to the prover).

When processing commands from a buffer for script management,
this will be set to the queue mode @code{'advancing} or @code{'retracting} to
indicate the direction of movement.

When this is non-nil, @samp{@code{proof-shell-ready-prover}} will give
an error if called with a different requested queue mode.

See also functions @samp{@code{proof-activate-scripting}} and
@samp{@code{proof-shell-available-p}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-marker
@defvar proof-marker 
Marker in proof shell buffer pointing to previous command input.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-action-list
@defvar proof-action-list 
The main queue of things to do: spans, commands and actions.@*
The value is a list of lists of the form
@lisp
   (@var{span} @var{commands} @var{action} [DISPLAYFLAGS])
@end lisp
which is the queue of things to do.

@var{span} is a region in the sources, where @var{commands} come from.  Often,
additional properties are recorded as properties of @var{span}.

@var{commands} is a list of strings, holding the text to be send to the
prover.  It might be the empty list if nothing needs to be sent to
the prover, such as, for comments.  Usually @var{commands}
contains just 1 string, but it might also contains more elements.
The text should be obtained with
@samp{(mapconcat }identity @var{commands} " ")', where the last argument
is a space.

@var{action} is the callback to be invoked when this item has been
processed by the prover. For normal scripting items it is
@samp{@code{proof-done-advancing}}, for retract items
@samp{@code{proof-done-retracting}}, but there are more possibilities (e.g.
@samp{@code{proof-done-invisible}}, @samp{@code{proof-shell-set-silent}},
@samp{@code{proof-shell-clear-silent}} and @samp{@code{proof-tree-show-goal-callback}}).

The @var{displayflags} are set
for non-scripting commands or for when scripting should not
bother the user.  They may include
@lisp
  @code{'invisible}                non-script command (@samp{@code{proof-shell-invisible-command}})
  @code{'no-response-display}      do not display messages in @strong{response} buffer
  @code{'no-error-display}         do not display errors/take error action
  @code{'no-goals-display}         do not goals in @strong{goals} buffer
  @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package
  @code{'priority-action}          item added via @code{proof-add-to-priority-queue}
@end lisp
Note that @code{'invisible} does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
printing hints).

See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}.
@end defvar

In Proof General 4.2 and earlier it was always the case that all
items from the queue region were present in
@code{proof-action-list}. Because of the new parallel background
compilation for Coq, this is no longer the case. Prover specific
code may now store items from the queue region somewhere else. To
notify generic Proof General about this, it must set
@code{proof-second-action-list-active} for the time where some
queue items are missing from @code{proof-action-list}. In this
case Proof General keeps the proof shell lock and the queue span
even in case @code{proof-action-list} gets empty. Coq uses this
feature to hold back Require commands and the following text
until the asynchronous background compilation finishes.

@c TEXI DOCSTRING MAGIC: proof-second-action-list-active
@defvar proof-second-action-list-active 
Signals that some items are waiting outside of @samp{@code{proof-action-list}}.@*
If this is t it means that some items from the queue region are
waiting for being processed in a place different from
@samp{@code{proof-action-list}}.  In this case Proof General must behave as if
@samp{@code{proof-action-list}} would be non-empty, when it is, in fact, empty.

This is used, for instance, for parallel background compilation
for Coq: The Require command and the following items are not put
into @samp{@code{proof-action-list}} and are stored somewhere else until the
background compilation finishes.  Then those items are put into
@samp{@code{proof-action-list}} for getting processed.
@end defvar

@c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack
@defvar pg-subterm-anns-use-stack 
Choice of syntax tree encoding for terms.

If nil, prover is expected to make no optimisations.
If non-nil, the pretty printer of the prover only reports local changes.
For Coq 6.2, use t.
@end defvar


The function @code{proof-shell-start} is used to initialise a shell
buffer and the associated buffers.  

@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn Command proof-shell-start 
Initialise a shell-like buffer for a proof assistant.@*
Does nothing if proof assistant is already running.

Also generates goal and response buffers.

If @samp{@code{proof-prog-name-ask}} is set, query the user for the
process command.
@end deffn

The function @code{proof-shell-kill-function} performs the converse
function of shutting things down; it is used as a hook function for
@code{kill-buffer-hook}.  Then no harm occurs if the user kills the
shell directly, or if it is done more cautiously via
@code{proof-shell-exit}.  The function @code{proof-shell-restart} allows
a less drastic way of restarting scripting, other than killing and
restarting the process.

@c TEXI DOCSTRING MAGIC: proof-shell-kill-function
@defun proof-shell-kill-function 
Function run when a proof-shell buffer is killed.@*
Try to shut down the proof process nicely and clear locked
regions and state variables.  Value for @samp{@code{kill-buffer-hook}} in
shell buffer, called by @samp{@code{proof-shell-bail-out}} if process exits.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-exit
@deffn Command proof-shell-exit &optional dont-ask
Query the user and exit the proof process.

This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function

@samp{@code{proof-shell-kill-function}} to do the hard work.  If optional
argument @var{dont-ask} is non-nil, the proof process is terminated
without confirmation.

The kill function uses @samp{<PA>-quit-timeout} as a timeout to wait
after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process.

This function should not be called if
@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of
@samp{@code{proof-shell-kill-function}} will give strange errors.
@end deffn

@c TEXI DOCSTRING MAGIC: proof-shell-bail-out
@defun proof-shell-bail-out process event
Value for the process sentinel for the proof assistant @var{process}.@*
If the proof assistant dies, run @samp{@code{proof-shell-kill-function}} to
cleanup and remove the associated buffers.  The shell buffer is
left around so the user may discover what killed the process.
@var{event} is the string describing the change.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-restart
@deffn Command proof-shell-restart 
Clear script buffers and send @samp{@code{proof-shell-restart-cmd}}.@*
All locked regions are cleared and the active scripting buffer
deactivated.

If the proof shell is busy, an interrupt is sent with
@samp{@code{proof-interrupt-process}} and we wait until the process is ready.

The restart command should re-synchronize Proof General with the proof
assistant, without actually exiting and restarting the proof assistant
process.

It is up to the proof assistant how much context is cleared: for
example, theories already loaded may be "cached" in some way,
so that loading them the next time round only performs a re-linking
operation, not full re-processing.  (One way of caching is via
object files, used by Coq).
@end deffn

@c
@c INPUT
@c
@subsection Input to the shell

Input to the proof shell via the queue region is managed by the
functions @code{proof-extend-queue} and @code{proof-shell-exec-loop}.

@c TEXI DOCSTRING MAGIC: proof-extend-queue
@defun proof-extend-queue end queueitems
Extend the current queue with @var{queueitems}, queue end @var{end}.@*
To make sense, the commands should correspond to processing actions
for processing a region from (buffer-queue-or-locked-end) to @var{end}.
The queue mode is set to @code{'advancing}
@end defun

@c TEXI DOCSTRING MAGIC: proof-extend-queue
@defun proof-extend-queue end queueitems
Extend the current queue with @var{queueitems}, queue end @var{end}.@*
To make sense, the commands should correspond to processing actions
for processing a region from (buffer-queue-or-locked-end) to @var{end}.
The queue mode is set to @code{'advancing}
@end defun
@vindex proof-action-list
@c TEXI DOCSTRING MAGIC: proof-shell-exec-loop
@defun proof-shell-exec-loop 
Main loop processing the @samp{@code{proof-action-list}}, called from shell filter.

@samp{@code{proof-action-list}} contains a list of (@var{span} @var{command} @var{action} [FLAGS]) lists.

If this function is called with a non-empty @samp{@code{proof-action-list}}, the
head of the list is the previously executed command which succeeded.
We execute the callback (@var{action} @var{span}) on the first item,
then (@var{action} @var{span}) on any following items which have null as
their cmd components.

If a there is a next command after that, send it to the process.

If the action list becomes empty, unlock the process and remove
the queue region.

The return value is non-nil if the action list is now empty or
contains only invisible elements for Prooftree synchronization.
@end defun

Input is actually inserted into the shell buffer and sent to the process
by the low-level function @code{proof-shell-insert}.  

@c TEXI DOCSTRING MAGIC: proof-shell-insert
@defun proof-shell-insert strings action &optional scriptspan
Insert @var{strings} at the end of the proof shell, call @samp{@code{scomint-send-input}}.

@var{strings} is a list of strings (which will be concatenated), or a
single string.

The @var{action} argument is a symbol which is typically the name of a
callback for when each string has been processed.

This calls @samp{@code{proof-shell-insert-hook}}.  The arguments @var{action} and
@var{scriptspan} may be examined by the hook to determine how to modify
the string variable (exploiting dynamic scoping) which will be
the command actually sent to the shell.

Note that the hook is not called for the empty (null) string
or a carriage return.

We strip the string of carriage returns before inserting it
and updating @samp{@code{proof-marker}} to point to the end of the newly
inserted text.

Do not use this function directly, or output will be lost.  It is only
used in @samp{@code{proof-add-to-queue}} when we start processing a queue, and in
@samp{@code{proof-shell-exec-loop}}, to process the next item.
@end defun


When Proof General is processing a queue of commands, the lock
is managed using a couple of utility functions.  You should
not need to use these directly.


@c TEXI DOCSTRING MAGIC: proof-grab-lock
@defun proof-grab-lock &optional queuemode
Grab the proof shell lock, starting the proof assistant if need be.@*
Runs @samp{@code{proof-state-change-hook}} to notify state change.
If @var{queuemode} is supplied, set the lock to that value.
@end defun

@c TEXI DOCSTRING MAGIC: proof-release-lock
@defun proof-release-lock 
Release the proof shell lock.  Clear @samp{@code{proof-shell-busy}}.
@end defun


@c
@c OUTPUT
@c
@subsection Output from the shell

Two main functions deal with output, @code{proof-shell-classify-output}
and @code{proof-shell-process-urgent-message}.  In effect we consider
the output to be two streams intermingled: the "urgent" messages which
have "eager" annotations, as well as the ordinary ruminations from the
prover.  

The idea is to conceal as much irrelevant information from the user as
possible; only the remaining output between prompts and after the last
urgent message will be a candidate for the goal or response buffer.  The
internal variable @code{proof-shell-urgent-message-marker} tracks the
last urgent message seen.

When output is grabbed from the prover process, the first action
is to strip spurious carriage return characters from the end of 
lines, if @code{proof-shell-strip-crs-from-output} requires it.
Then the output is stored into
@code{proof-shell-last-output}, and its type is stored in
@code{proof-shell-last-output-kind}.  Output which is deferred or
possibly discarded until the queue is empty is copied into
@code{proof-shell-delayed-output}, with type
@code{proof-shell-delayed-output-kind}.  A record of the last prompt
seen from the prover process is also kept, in
@code{proof-shell-last-prompt}.


@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-output
@defvar proof-shell-strip-crs-from-output 
If non-nil, remove carriage returns (^M) at the end of lines from output.@*
This is enabled for cygwin32 systems by default.  You should turn it off
if you don't need it (slight speed penalty).
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-last-prompt
@defvar proof-shell-last-prompt 
A raw record of the last prompt seen from the proof system.@*
This is the string matched by @samp{@code{proof-shell-annotated-prompt-regexp}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-last-output
@defvar proof-shell-last-output 
A record of the last string seen from the proof system.@*
This is raw string, for internal use only.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-last-output-kind
@defvar proof-shell-last-output-kind 
A symbol denoting the type of the last output string from the proof system.@*
Specifically:
@lisp
 @code{'interrupt}      An interrupt message
 @code{'error}          An error message
 @code{'loopback}       A command sent from the PA to be inserted into the script
 @code{'response}       A response message
 @code{'goals}          A goals (proof state) display
 @code{'systemspecific} Something specific to a particular system,
                  -- see @samp{@code{proof-shell-handle-output-system-specific}}
@end lisp
The output corresponding to this will be in @samp{@code{proof-shell-last-output}}.

See also @samp{@code{proof-shell-proof-completed}} for further information about
the proof process output, when ends of proofs are spotted.

This variable can be used for instance specific functions which want
to examine @samp{@code{proof-shell-last-output}}.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-last-output-kind
@defvar proof-shell-last-output-kind 
A symbol denoting the type of the last output string from the proof system.@*
Specifically:
@lisp
 @code{'interrupt}      An interrupt message
 @code{'error}          An error message
 @code{'loopback}       A command sent from the PA to be inserted into the script
 @code{'response}       A response message
 @code{'goals}          A goals (proof state) display
 @code{'systemspecific} Something specific to a particular system,
                  -- see @samp{@code{proof-shell-handle-output-system-specific}}
@end lisp
The output corresponding to this will be in @samp{@code{proof-shell-last-output}}.

See also @samp{@code{proof-shell-proof-completed}} for further information about
the proof process output, when ends of proofs are spotted.

This variable can be used for instance specific functions which want
to examine @samp{@code{proof-shell-last-output}}.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-start
@defvar proof-shell-delayed-output-start 
A record of the start of the previous output in the shell buffer.@*
The previous output is held back for processing at end of queue.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-end
@defvar proof-shell-delayed-output-end 
A record of the start of the previous output in the shell buffer.@*
The previous output is held back for processing at end of queue.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-flags
@defvar proof-shell-delayed-output-flags 
A copy of the @samp{@code{proof-action-list}} flags for @samp{proof-shell-delayed-output}.
@end defvar
@vindex proof-action-list

@c TEXI DOCSTRING MAGIC: proof-shell-handle-immediate-output
@defun proof-shell-handle-immediate-output cmd start end flags
See if the output between @var{start} and @var{end} must be dealt with immediately.@*
To speed up processing, PG tries to avoid displaying output that
the user will not have a chance to see.  Some output must be
handled immediately, however: these are errors, interrupts,
goals and loopbacks (proof step hints/proof by pointing results).

In this function we check, in turn:
@lisp
  @samp{@code{proof-shell-interrupt-regexp}}
  @samp{@code{proof-shell-error-regexp}}
  @samp{@code{proof-shell-proof-completed-regexp}}
  @samp{@code{proof-shell-result-start}}
@end lisp
Other kinds of output are essentially display only, so only
dealt with if necessary.

To extend this, set @samp{@code{proof-shell-handle-output-system-specific}},
which is a hook to take particular additional actions.

This function sets variables: @samp{@code{proof-shell-last-output-kind}},
and the counter @samp{@code{proof-shell-proof-completed}} which counts commands
after a completed proof.
@end defun


@c TEXI DOCSTRING MAGIC: proof-shell-handle-delayed-output
@defun proof-shell-handle-delayed-output 
Display delayed goals/responses, when queue is stopped or completed.@*
This function handles the cases of @samp{proof-shell-output-kind} which
are not dealt with eagerly during script processing, namely
@code{'response} and @code{'goals} types.

This is useful even with empty delayed output as it will empty
the buffers.

The delayed output is in the region
[@code{proof-shell-delayed-output-start},@code{proof-shell-delayed-output-end}].

If no goals classified output is found, the whole output is
displayed in the response buffer.

If goals output is found, the last matching instance, possibly
bounded by @samp{@code{proof-shell-end-goals-regexp}}, will be displayed
in the goals buffer (and may be further analysed by Proof General).

Any output that appears @strong{before} the last goals output (but
after messages classified as urgent, see @samp{@code{proof-shell-filter}})
will also be displayed in the response buffer.

For example, if @var{output} has this form:
@lisp
  @var{messsage-1}
  @var{goals-1}
  @var{message-2}
  @var{goals-2}
  @var{junk}
@end lisp
then @var{goals-2} will be displayed in the goals buffer, and @var{message-2}
in the response buffer.  @var{junk} will be ignored.

Notice that the above alternation (and separation of @var{junk}) can
only be distinguished if both @samp{@code{proof-shell-start-goals-regexp}}
and @samp{@code{proof-shell-end-goals-regexp}} are set.  With just the start
goals regexp set, @var{goals-2} @var{junk} will appear in the goals buffer
and no response output would occur.
@lisp
@end lisp
The goals and response outputs are copied into
@samp{@code{proof-shell-last-goals-output}} and
@samp{@code{proof-shell-last-response-output}} respectively.

The value returned is the value for @samp{@code{proof-shell-last-output-kind}},
i.e., @code{'goals} or @code{'response}.
@end defun
@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker
@defvar proof-shell-urgent-message-marker 
Marker in proof shell buffer pointing to end of last urgent message.
@end defvar

@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message
@defun proof-shell-process-urgent-message start end
Analyse urgent message between @var{start} and @var{end} for various cases.

Cases are: @strong{trace} output, included/retracted files, cleared
goals/response buffer, variable setting, xml-encoded @var{pgip} response,
theorem dependency message or interactive output indicator.

If none of these apply, display the text between @var{start} and @var{end}.

The text between @var{start} and @var{end} should be a string that starts with
text matching @samp{@code{proof-shell-eager-annotation-start}} and
ends with text matching @samp{@code{proof-shell-eager-annotation-end}}.
@end defun

The main processing point which triggers other actions is
@code{proof-shell-filter}. It is called from
@code{proof-shell-filter-wrapper}, which itself is called from an
ordinary Emacs process filter inside the simplified @code{comint}
library that is distributed with Proof General (in
@code{lib/scomint.el}).

@c TEXI DOCSTRING MAGIC: proof-shell-filter
@defun proof-shell-filter 
Master filter for the proof assistant shell-process.@*
A function for @samp{@code{scomint-output-filter-functions}}.

Deal with output and issue new input from the queue.  This is an
important internal function.  The output must be collected from
@samp{@code{proof-shell-buffer}} for the following reason.  This function
might block inside @samp{@code{process-send-string}} when sending input to
the proof assistant or to prooftree.  In this case Emacs might
call the process filter again while the previous instance is
still running.  @samp{@code{proof-shell-filter-wrapper}} detects and delays
such calls but does not buffer the output.

Handle urgent messages first.  As many as possible are processed,
using the function @samp{@code{proof-shell-process-urgent-messages}}.

If a prompt is seen, run @samp{@code{proof-shell-filter-manage-output}} on the
output between the new prompt and the last input (position of
@samp{@code{proof-marker}}) or the last urgent message (position of
@samp{@code{proof-shell-urgent-message-marker}}), whichever is later.  For
example, in this case:
@lisp
 PROMPT> @var{input}
 @var{output-1}
 @var{urgent-message-1}
 @var{output-2}
 @var{urgent-message-2}
 @var{output-3}
 PROMPT>
@end lisp
@samp{@code{proof-marker}} points after @var{input}.

@samp{@code{proof-shell-urgent-message-marker}} points after @var{urgent-message-2},
after both urgent messages have been processed by
@samp{@code{proof-shell-process-urgent-messages}}.  Urgent messages always
processed; they are intended to correspond to informational
notes that the prover makes to inform the user or interface on
progress.

In this case, the ordinary outputs @var{output-1} and @var{output-2} are
ignored; only @var{output-3} will be processed by
@samp{@code{proof-shell-filter-manage-output}}.

Error or interrupt messages are expected to terminate an
interactive output and appear last before a prompt and will
always be processed.  Error messages and interrupt messages are
therefore @strong{not} considered as urgent messages.

The first time that a prompt is seen, @samp{@code{proof-marker}} is
initialised to the end of the prompt.  This should correspond
with initializing the process.  After that, @samp{@code{proof-marker}}
is only changed when input is sent in @samp{@code{proof-shell-insert}}.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-filter-manage-output
@defun proof-shell-filter-manage-output start end
Subroutine of @samp{@code{proof-shell-filter}} for output between @var{start} and @var{end}.

First, we invoke @samp{@code{proof-shell-handle-immediate-output}} which classifies
and handles output that must be dealt with immediately.

Other output (user display) is only displayed when the proof
action list becomes empty, to avoid a confusing rapidly changing
output that slows down processing.

After processing the current output, the last step undertaken
by the filter is to send the next command from the queue.
@end defun

@c TEXI DOCSTRING MAGIC: proof-shell-filter-wrapper
@defun proof-shell-filter-wrapper str-do-not-use
Wrapper for @samp{@code{proof-shell-filter}}, protecting against parallel calls.@*
In Emacs a process filter function can be called while the same
filter is currently running for the same process, for instance,
when the filter blocks on I/O. This wrapper protects the main
entry point, @samp{@code{proof-shell-filter}} against such parallel,
overlapping calls.

The argument @var{str-do-not-use} contains the most recent output, but
is discarded. @samp{@code{proof-shell-filter}} collects the output from
@samp{@code{proof-shell-buffer}} (where it is inserted by
@samp{@code{scomint-output-filter}}), relieving this function from the task
to buffer the output that arrives during parallel, overlapping
calls.
@end defun



@c
@c SECTION: Debugging
@c
@node Debugging
@section Debugging
@cindex debugging

@c FIXME: better to have general hints on Elisp earlier, plus some
@c links to helpful docs.

To debug Proof General, it may be helpful to set the
configuration variable @code{proof-general-debug}.

@c TEXI DOCSTRING MAGIC: proof-general-debug
@defopt proof-general-debug 
Non-nil to run Proof General in debug mode.@*
This changes some behaviour (e.g. markup stripping) and displays
debugging messages in the response buffer.  To avoid erasing
messages shortly after they're printed, set @samp{@code{proof-tidy-response}} to nil.
This is only useful for PG developers.

The default value is @code{nil}.
@end defopt

For more information about debugging Emacs lisp, consult the Emacs Lisp
Reference Manual.  I recommend using the source-level debugger
@code{edebug}.














@c
@c
@c APPENDIX: Plans and Ideas
@c
@c
@node Plans and Ideas
@appendix Plans and Ideas

This appendix contains some tentative plans and ideas for improving
Proof General.

This appendix is no longer extended: instead we keep a list of Proof
General projects on the web, and forthcoming plans and ideas in the
@file{TODO} and @file{todo} files included in the ordinary and
developers PG distributions, respectively.  Once the items mentioned
below are implemented, they will be removed from here.

Please send us contributions to our wish lists, or better still, an
offer to implement something from them!

@menu
* Proof by pointing and similar features::
* Granularity of atomic command sequences::  
* Browser mode for script files and theories::  
@end menu

@node Proof by pointing and similar features
@section Proof by pointing and similar features
@cindex proof by pointing

This is a note by David Aspinall about proof by pointing and similar
features.

Proof General already supports proof by pointing, and experimental
support was provided in LEGO.  We would like to extend this support to
other proof assistants.  Unfortunately, proof by pointing requires
rather heavy support from the proof assistant.  There are two aspects to
the support:
@itemize @bullet
@item term structure mark-up
@item proof by pointing command generation
@end itemize
Term structure mark-up is useful in itself: it allows the user to
explore the structure of a term using the mouse (the smallest
subexpression that the mouse is over is highlighted), and easily copy
subterms from the output to a proof script.

Command generation for proof by pointing is usually specific to a
particular logic in use, if we hope to generate a good proof command
unambiguously for any particular click. However, Proof General could
easily be generalised to offer the user a context-sensitive choice of
next commands to apply, which may be more useful in practice, and a
worthy addition to Proof General.

Implementors of new proof assistants should be encouraged to consider
supporting term-structure mark up from the start.  Command generation
should be something that the logic-implementor can specify in some way.

Of the supported provers, we can certainly hope for proof-by-pointing
support from Coq, since the CtCoq proof-by-pointing code has been moved
into the Coq kernel lately.  I hope the Coq community can encourage
somebody to do this.


@node Granularity of atomic command sequences
@section Granularity of atomic command sequences
@c @cindex Granularity of Atomic Sequences
@c @cindex Retraction
@c @cindex Goal
@cindex ACS (Atomic Command Sequence)

This is a proposal by Thomas Kleymann for generalising the way Proof
General handles sequences of proof commands (see @i{Goal-save
sequences} in the user manual), particularly to make retraction more flexible.

The blue region of a script buffer contains the initial segment of
the proof script which has been processed successfully. It consists of
atomic sequences of commands (ACS). Retraction is supported to the
beginning of every ACS. By default, every command is an ACS. But the
granularity of atomicity should be able to be adjusted.

This is essential when arbitrary retraction is not supported. Usually,
after a theorem has been proved, one may only retract to the start of
the goal. One needs to mark the proof of the theorem as an ACS. At
present, support for goal-save sequences (see @i{Goal-save sequences} in
the user manual), has been hard wired. No other ACS are currently
supported. We propose the following to overcome this deficiency:

@vtable @code
@item proof-atomic-sequents-list
is a list of instructions for setting up ACSs. Each instruction is a
list of the form @code{(@var{end} @var{start} &optional
@var{forget-command})}. @var{end} is a regular expression to recognise
the last command in an ACS. @var{start} is a function. Its input is the
last command of an ACS. Its output is a regular expression to recognise
the first command of the ACS. It is evaluated once and, starting with the
command matched by @var{end}, the output is
successively matched against previously processed commands until a match
occurs (or the beginning of the current buffer is reached). The region
determined by (@var{start},@var{end}) is locked as an ACS. Optionally,
the ACS is annotated with the actual command to retract the ACS. This is 
computed by applying @var{forget-command} to the first and last command
of the ACS.

For convenience one might also want to allow @var{start} to be the
symbol @samp{t} as a convenient short-hand for @code{'(lambda (str)
".")} which always matches.
@end vtable

@node Browser mode for script files and theories
@section Browser mode for script files and theories

This is a proposal by David Aspinall for a browser window.

A browser window should provide support for browsing script files and
theories.  We should be able to inspect data in varying levels of
detail, perhaps using outlining mechanisms.  For theories, it would be
nice to query the running proof assistant.  This may require support
from the assistant in the form of output which has been specially
marked-up with an SGML like syntax, for example.

A browser would be useful to:
@itemize @bullet
@item Provide impoverished proof assistants with a browser
@item Extend the uniform interface of Proof General to theory browsing 
@item Interact closely with proof script writing
@end itemize
The last point is the most important. We should be able to integrate a
search mechanism for proofs of similar theorems, theorems containing
particular constants, etc.




@c
@c
@c APPENDIX: Demonstration instantiation for Isabelle
@c
@c
@node Demonstration Instantiations
@appendix Demonstration Instantiations

This appendix contains the code for the two demonstration
instantiations of Proof General, for Isabelle.

These instantiations make an almost-bare minimum of settings to get
things working.  To add embellishments, you should refer to
the instantiations for other systems distributed with
Proof General.

@menu
* demoisa-easy.el::
* demoisa.el::
@end menu

@node demoisa-easy.el
@section demoisa-easy.el

@lisp
@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM
@c @includeverbatim ../demoisa/demoisa-easy.el
;; demoisa-easy.el Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh. 
;;
;; Author: David Aspinall <David.Aspinall@@ed.ac.uk>
;;
;; $Id$
;;
;; This is an alternative version of demoisa.el which uses the
;; proof-easy-config macro to do the work of declaring derived modes,
;; etc.  
;;
;; See demoisa.el and the Proof General manual for more documentation.
;;
;; To test this file you must rename it demoisa.el.
;;

(require 'proof-easy-config)            ; easy configure mechanism

(proof-easy-config 
 'demoisa "Isabelle Demo" 
 proof-prog-name		 "isabelle"
 proof-terminal-string           ";"
 proof-script-comment-start             "(*"
 proof-script-comment-end               "*)"
 proof-goal-command-regexp       "^Goal"
 proof-save-command-regexp       "^qed"
 proof-goal-with-hole-regexp     "qed_goal \"\\(\\(.*\\)\\)\""
 proof-save-with-hole-regexp     "qed \"\\(\\(.*\\)\\)\""
 proof-non-undoables-regexp      "undo\\|back"
 proof-goal-command              "Goal \"%s\";"
 proof-save-command              "qed \"%s\";"
 proof-kill-goal-command         "Goal \"PROP no_goal_set\";"
 proof-showproof-command         "pr()"
 proof-undo-n-times-cmd          "pg_repeat undo %s;"
 proof-auto-multiple-files       t
 proof-shell-cd-cmd              "cd \"%s\""
 proof-shell-interrupt-regexp    "Interrupt"
 proof-shell-start-goals-regexp  "Level [0-9]"
 proof-shell-end-goals-regexp    "val it"
 proof-shell-quit-cmd            "quit();"
 proof-assistant-home-page    
 "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
 proof-shell-annotated-prompt-regexp 
 "^\\(val it = () : unit\n\\)?ML>? "
 proof-shell-error-regexp             
 "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
 proof-shell-init-cmd  
 "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
 proof-shell-proof-completed-regexp "^No subgoals!"
 proof-shell-eager-annotation-start   
 "^\\[opening \\|^###\\|^Reading")

(provide 'demoisa)
@end lisp

@node demoisa.el
@section demoisa.el

@lisp
@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM
@c @includeverbatim ../demoisa/demoisa.el
;; demoisa.el Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh. 
;;
;; Author: David Aspinall <David.Aspinall@@ed.ac.uk>
;;
;; $Id$
;;
;; =================================================================
;;
;; See README in this directory for an introduction.
;;
;; Basic configuration is controlled by one line in `proof-site.el'.
;; It has this line in proof-assistant-table:
;;
;;     (demoisa "Isabelle Demo"	"\\.ML$")
;;
;; From this it loads this file "demoisa/demoisa.el" whenever
;; a .ML file is visited, and sets the mode to `demoisa-mode'
;; (defined below).  
;; 
;; I've called this instance "Isabelle Demo Proof General" just to
;; avoid confusion with the real "Isabelle Proof General" in case the
;; demo gets loaded by accident.
;;
;; To make the line above take precedence over the real Isabelle mode
;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the
;; shell before starting Emacs  (or customize proof-assistants).
;;


(require 'proof)			; load generic parts


;; ======== User settings for Isabelle ========
;;
;; Defining variables using customize is pretty easy.
;; You should do it at least for your prover-specific user options.
;;
;; proof-site provides us with two customization groups
;; automatically:  (based on the name of the assistant)
;;
;; 'isabelledemo        -  User options for Isabelle Demo Proof General
;; 'isabelledemo-config -  Configuration of Isabelle Proof General
;;			   (constants, but may be nice to tweak)
;;
;; The first group appears in the menu
;;   ProofGeneral -> Advanced -> Customize -> Isabelledemo 
;; The second group appears in the menu:
;;   ProofGeneral -> Internals -> Isabelledemo config
;;

(defcustom isabelledemo-prog-name "isabelle"
  "*Name of program to run Isabelle."
  :type 'file
  :group 'isabelledemo)

(defcustom isabelledemo-web-page
  "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
  "URL of web page for Isabelle."
  :type 'string
  :group 'isabelledemo-config)


;;
;; ======== Configuration of generic modes ========
;;

(defun demoisa-config ()
  "Configure Proof General scripting for Isabelle."
  (setq
   proof-terminal-string	";"
   proof-script-comment-start	"(*"
   proof-script-comment-end	"*)"
   proof-goal-command-regexp    "^Goal"
   proof-save-command-regexp    "^qed"
   proof-goal-with-hole-regexp  "qed_goal \"\\(\\(.*\\)\\)\""
   proof-save-with-hole-regexp  "qed \"\\(\\(.*\\)\\)\""
   proof-non-undoables-regexp   "undo\\|back"
   proof-undo-n-times-cmd	"pg_repeat undo %s;"
   proof-showproof-command	"pr()"
   proof-goal-command		"Goal \"%s\";"
   proof-save-command		"qed \"%s\";"
   proof-kill-goal-command	"Goal \"PROP no_goal_set\";"
   proof-assistant-home-page	isabelledemo-web-page
   proof-auto-multiple-files    t))


(defun demoisa-shell-config ()
  "Configure Proof General shell for Isabelle."
  (setq
   proof-shell-annotated-prompt-regexp   "^\\(val it = () : unit\n\\)?ML>? "
   proof-shell-cd-cmd			"cd \"%s\""
   proof-shell-interrupt-regexp         "Interrupt"
   proof-shell-error-regexp		"\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
   proof-shell-start-goals-regexp	"Level [0-9]"
   proof-shell-end-goals-regexp		"val it"
   proof-shell-proof-completed-regexp   "^No subgoals!"
   proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading"
   proof-shell-init-cmd  ; define a utility function, in a lib somewhere?
   "fun pg_repeat f 0 = () 
      | pg_repeat f n = (f(); pg_repeat f (n-1));"
   proof-shell-quit-cmd			"quit();"))



;;
;; ======== Defining the derived modes ========
;;

;; The name of the script mode is always <proofsym>-script,
;; but the others can be whatever you like.
;;
;; The derived modes set the variables, then call the
;; <mode>-config-done function to complete configuration.

(define-derived-mode demoisa-mode proof-mode
    "Isabelle Demo script" nil
    (demoisa-config)
    (proof-config-done))

(define-derived-mode demoisa-shell-mode proof-shell-mode
   "Isabelle Demo shell" nil
   (demoisa-shell-config)
   (proof-shell-config-done))

(define-derived-mode demoisa-response-mode proof-response-mode
  "Isabelle Demo response" nil
  (proof-response-config-done))

(define-derived-mode demoisa-goals-mode proof-goals-mode
  "Isabelle Demo goals" nil
  (proof-goals-config-done))

;; The response buffer and goals buffer modes defined above are
;; trivial.  In fact, we don't need to define them at all -- they
;; would simply default to "proof-response-mode" and "pg-goals-mode".

;; A more sophisticated instantiation might set font-lock-keywords to
;; add highlighting, or some of the proof by pointing markup
;; configuration for the goals buffer.

(provide 'demoisa)
@end lisp




@node Function Index
@unnumbered Function and Command Index
@printindex fn

@node Variable Index
@unnumbered Variable and User Option Index
@printindex vr

@c Nothing in this one!
@c @node Keystroke Index
@c @unnumbered Keystroke Index
@c @printindex ky

@node Concept Index
@unnumbered Concept Index
@printindex cp

@page
@contents
@bye