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.4, this support has existed only 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-goals-button-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-and-delete-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.

Command: pg-goals-button-action event

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.

Command: pg-identifier-under-mouse-query event: Query the prover about the identifier near mouse click event.

This document was generated on April 20, 2024 using texi2html 1.82.