Download User manual - Proof General

Chapter 6: Subterm Activation and Proof by Pointing
37
6 Subterm Activation and Proof by Pointing
This chapter describes what you can do from inside the goals buffer, providing support for these
features exists for your proof assistant.
As of Proof General 4.0, this support only exists for LEGO and proof-by-pointing functionality
has been temporarily removed from the interface. If you would like to see subterm activation
support for Proof General in another proof assistant, please petition the developers of that proof
assistant to provide it!
6.1 Goals buffer commands
When you are developing a proof, the input focus (Emacs cursor) is usually on the script buffer.
Therefore Proof General binds some mouse buttons for commands in the goals buffer, to avoid
the need to move the cursor between buffers.
The mouse bindings are these:
mouse-1
pg-goals-button-action
C-mouse-3
proof-undo-and-delete-last-successful-command
C-S-mouse-1
pg-identifier-under-mouse-query
Where mouse-1 indicates the left mouse button, and mouse-3 indicates the right hand mouse
button. The functions available provide a way to construct commands automatically (pg-goalsbutton-action) and to inspect identifiers (pg-identifier-under-mouse-query) as the Info
toolbar button does.
Proof-by-pointing is a cute idea. It lets you automatically construct parts of a proof by clicking.
You can ask the proof assistant to try to do a step in the proof, based on where you click. If you
don’t like the command which was inserted into the script, you can comment use the control
key with the right button to undo the step and delete it from your script (proof-undo-anddelete-last-successful-command).
Proof-by-pointing may construct several commands in one go. These are sent back to the proof
assistant altogether and appear as a single step in the proof script. However, if the proof is
later replayed (without using PBP), the proof-by-pointing constructions will be considered as
separate proof commands, as usual.
The main function for proof-by-pointing is pg-goals-button-action.
pg-goals-button-action event
[Command]
Construct a proof-by-pointing command based on the mouse-click event.
This function should be bound to a mouse button in the Proof General goals buffer.
The event is used to find the smallest subterm around a point. A position code for the
subterm is sent to the proof assistant, to ask it to construct an appropriate proof command.
The command which is constructed will be inserted at the end of the locked region in the
proof script buffer, and immediately sent back to the proof assistant. If it succeeds, the
locked region will be extended to cover the proof-by-pointing command, just as for any proof
command the user types by hand.
Proof-by-pointing uses markup describing the term structure of the concrete syntax output by
the proof assistant. This markup is useful in itself: it allows you 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.