Drawback of command wrapping in PG+Isar

[David Aspinall]

[message from Lucas Dixon]

(PG: 4.0pre090916) I used to sprinkle semi-colon's around my theory files so that I could quickly introduce new syntax. I noticed recently that this now has some annoying behaviour:

; ;

now produces:

*** Outer syntax error: exactly one command expected

It would be nicer (for me) if it still treated ";" as a command separator, and let them have whitespace between.

The same error crops up in a couple of other places:

type:

ML{*
val _ = 1;
*}

process this then add:

;
ML{*
val _ = 2;
*}

same error.

Also:

(*foo*)
;

[David Aspinall]

[Followup from Makarius]:

I have already noticed that the Isabelle.command wrapper is a bit picky in insisting in exactly one command. This is not easy to generalize to several commands, although that might be useful for certain internal "Isar code generation" functions in elisp (like undos or PGIP commands).

Having said that, I could imagine a slightly smarter version of Isabelle.command that filters out "empty" commands stemming from semicolons. Of course that would not help for Isabelle2009, but Lucas is working with some repository version anyway.

[David Aspinall]

[Second followup from Makarius]:

In fact, Isabelle2009 is already smart enough to ignore extra semicolons within commands.

It seems it is again a problem of "cursor movement" in PG. Try this:

  term x;

  term y;

If you move carefully forward via proof-assert-next-command-interactive two times, it works as expected.

Instead, after retracting both, if you move the point after the semicolon of term x and do proof-assert-until-point-interactive, the error occurs. This is because PG sends an extra "empty" command consisting of the white space after the semicolon, until the next command.

[David Aspinall]

Fixed in proof-script.el 10.44, which makes proof-cmdstart-add-segment-for-cmd classify whitespace as a comment, not a command.

[David Aspinall]

On the other hand, sending two semi-colons separated by space still causes Isabelle to complain: Proof General does not try to enforce that there must be some text before the semi-colon.

\<^sync>; Isabelle.command ("file"="/home/da/PG/etc/isar/EmptyCommands.thy", "line"="5") "; ;"; \<^sync>;
*** Outer syntax error: exactly one command expected