Allow use of Isabelle.command to wrap commands singly

[David Aspinall]

Isabelle.command allows additional "properties" to be attached to individual commands when they are processed by Isar. Example properties are file name and line number (Isabelle Position type), which are not maintained by the top-level loop, but would be useful to get error messages to include this information when processing interactively.

[Makarius]

The attached version of isar.el implements basic wrapping of commands, without any position information yet. Nevertheless, it helps to avoid synchronization problems (with malformed tokens like -- "\bad").

Note: PG tends to paste several commands together internally, which is incompatible with the singleton wrapping; e.g. undo sequences.

[David Aspinall]

Updated patch for command wrapping

[David Aspinall]

Remark: attached a patch with just this change.

Breaking apart conjoined undo commands is possible in principle but requires considerable reworking because then each undo step must then carry the distance that it undoes, and this change would need to be made in every prover.

Since we only need this for the degenerate case of control ("improper", non proof-script) commands which do not require position information, could we instead add a different wrapper for those ones, which allows several commands? Something like Isabelle.controlcommands.

[David Aspinall]

Remark: version 10.9 of isar.el now adds a slightly modified version of this patch. To avoid the problem with sequences of commands it does not wrap any that look like undo commands. Note: "look like" is approximate as the regexp could be fooled.

I have a partial patch for a more robust solution, which allows batching up a sequence of commands to send. This is still in progress as is actually passing some useful position information.

[David Aspinall]

Position information is now passed to Isabelle.

Line and file numbers are reported back enthusiastically by Isabelle in error messages, but it seems that column numbers are not.