Undo on edit in ML-sections

[Alexander Krauss]

It appears that undo-on-edit does not work when editing within an ML {* ... *}-section.

[David Aspinall]

That's correct. It's because the syntax tables for Isar categorise these sections as comments and Proof General considers comments as not affecting the state, and so may be freely edited without requiring undo.

Thanks for adding the ticket. I'll push this onto the list for PG 4.1, for the time being suggest work around of hitting C-c C-RET when you edit in an ML section.

[Makarius]

This syntax categorization is merely an old workaround, so that Emacs treats the {* verbatim text *} category of Isabelle almost correctly. The meaning of "comment" has hard to guess from the editor side, so I would prefer if Proof General would just pass through to the prover, without attempting to interpret syntax.

For 4.0: maybe one could just use strict read-only by default.

[David Aspinall]

Remark to above comment: this concerns the internal part of a command which is already sent to Isabelle. The point is that the internal part of it is considered as if it were a comment.

This is certainly convenient for true comments. For ML sections (already advanced users!), I think it's not too bad to live with this and have folk hit a key.