5. Listening (and talking)

A listener buffer receives a verbatim copy of every command that is issued to an Isabelle session. It is useful for recording interactive proofs: you can cut and paste lines into an ML file to store proofs. Listener buffers can now also talk: you can type commands directly into them, and send lines to the Isabelle session. This makes it easy to create proof scripts.

The command to create a listener buffer is M-x listener. It is usually bound to C-c M-l, which is useful in single frame mode, or to clear the listener buffer when you start a fresh proof.

Command: listener

Start a new listener buffer associated with the current Isabelle interaction buffer. This gives an error if the current buffer is not an Isabelle interaction buffer.

In fact, it is possible for any buffer to be treated as a listener, and you can easily turn listening on and off. This makes it easy to write proof scripts directly into `.ML' files.

Command: listener-minor-mode

Toggle listening for the current buffer.

5.1 Listener Commands

The listener minor mode provides functions useful for editing proof scripts; you can mix and match typing in the buffer that "listens" with typing in and using menus from the Isabelle process buffer.

You can send command lines from a listener buffer to the associated Isabelle process using C-c C-l or C-c C-n (which runs listener-use-line). This copies text from the start of the line, up to the next semi-colon that isn't enclosed in a string or comment. See section 6.2 Editing ML files for further details of a similar command in ML buffers.

Another way of sending lines to the Isabelle process is by pasting them into a listener buffer with C-c C-y (listener-yank-and-use), instead of just C-y. This is like yanking the text, going to the beginning of the line, and using C-c C-n.

You can send an "undo" command to the Isabelle process with C-c C-u or C-c C-p (listener-use-line). After sending the undo, this attempts to move backwards to the previous interactive command.

The movement functions alone are available with C-c C-f (isa-forward-interactive-line) and C-c C-b (isa-backward-interactive-line).

Two other commands useful inside the listener are isa-batchify and isa-unbatchify, which let you very easily create batch proofs from interactive ones and vise-versa. See section 6.3 Interactive and Batch Proofs. This makes dedicated listener buffers most useful for playing back batched forms of interactive proofs. For example, you could copy a batch proof from a file into the listener, unbatchify it, and then watch it replay step by step using C-c C-n.

Go to the first, previous, next, last section, table of contents.