Goal buffer not updated on "undo" and "goto

[Alexander Krauss]

in 4.0pre090921 under GNU Emacs 23.1.1

at these commands, the goal buffer stays the same. For example, to go back one step and update the goal buffer, I must actually go back two steps and then one step forward.

[David Aspinall]

Thanks for the report. Assume you are using Isabelle with the new linear_undo command. Unfortunately the "linear_undo" command does not print out the current state.

Have added "pr" now to the command, which improves this.

Unfortunately it prints nothing if there is no state, whereas we would prefer that it cleared the display. I'm not sure how to do this without delving into internals of Isar.

[Makarius]

In the old protocol with non-linear undo, it worked via the kill_proof command that was issued instead of undo here. As can be seen in ​http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/src/Pure/ProofGeneral/proof_general_emacs.ML#l95 and ​http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/src/Pure/ProofGeneral/proof_general_emacs.ML#l201 Proof General is told explicitly to clear the goal area.

[David Aspinall]

Thanks for followup, but not sure why reopened. Point is that previously PG tracked in/out of proof status and issued different commands, I think linear_undo should be more stupid, just sending the number of commands to undo. I think the ideal is to provide an Isar-level wrapper for linear_undo which redisplays the relevant output, or clears goals. Don't know how to do that.

[David Aspinall]

Fixed for Isabelle2009-1 and beyond: now PG uses ProofGeneral.pr command when available. Undo printing behaviour for older Isabelle versions will be better without linear undo.