The proof state buffer maintains a display of the current proof state (goal and subgoal list) during interactive proof. Usually this would appear interspersed with user input on the terminal -- one of the major benefits of using Isamode is that it separates this output and keeps the machine dialogue uncluttered.
Internally, this is implemented by setting up a process-filter which
watches output from the Isabelle process, waiting for character
sequences that look like displays of the proof state, as for example,
when you type pr();. If a proof state buffer is active, these
sequences will be stripped from the output and used to update the
buffers contents.
M-x proofstate is usually bound to C-c M-p, which is useful in single frame mode (see section 7.1 Display options) because it provides a quick way of switching buffers in another window to show the proofstate display.
In the proof state buffer, the cursor usually appears opposite one of the subgoals in the list (if there are any). This subgoal is called the designated subgoal; it can be selected using the cursor keys up and down, or from the interaction buffer, with C-up and C-down.
The designated subgoal is the one you wish to prove; it is the subgoal that will be used by default by the tactic insertion commands in the interaction buffer (See section 2.6 Interaction mode menu operations.) or in a rule table (see section 4.1 Ruletable Commands)
Other useful keys in the proofstate buffer are LEFT
(proofstate-previous-level) and RIGHT
(proofstate-next-level), which page back and forward through
levels of the proof. To go directly to a specific level, type the level
as a prefix argument (e.g., M-2 M-7 for level 27), and hit
SPC (proofstate-refresh). Without an argument,
proofstate-refresh returns to the latest level.
If you resize the proofstate window, it is useful to set Isabelle's
pretty printer margin appropriately. This is done by pressing RET
(proofstate-resize-and-refresh).
You may discover that very large proof states sometimes fail to parse and end up in the Isabelle buffer, instead of the proof state buffer.
The reason for this is that the Emacs code filters all the output from
the Isabelle process so that proof states can be stripped out. This is
done by matching on text between ML prompts; text up to the next prompt
is put into a hidden output buffer before matching. Unfortunately, this
has a bad interaction with use and use_thy, because
use may produce a lot of output (perhaps slowly) before the next
prompt appears, and it is very strange not to see any output before
use has finished.
So if the output gets larger than a certain threshold, Isamode assumes
that it is from use (or something similar), and won't contain a
proof state. The variable that controls this threshold is
isa-text-spill-size, which defaults to 2000. If you
notice large proof states spilling into the Isabelle buffer, one
solution is to reduce the goals limit; another is to
set this variable higher by, for example:
(setq isa-text-spill-size 5000)
in your `.emacs'. But remember that there will be a bigger delay
with use.
The present output filtering technique is unsatisfactory and may be changed in the future when improved mechanisms of communication between Isabelle and Emacs are possible.
Go to the first, previous, next, last section, table of contents.