Semi-colons (';') cause outer syntax error: one command expected

[Lucas Dixon]

Using semi-colons used to be a handy way to control Proof General's parser, to stop it from going over all comments in one step.

However, using semi-colons on PG version 4.0pre100825 causes an error. E.g.

theory Scratch
imports Main 
begin 

-- "a comment"
;
-- "another comment that PG does not get to"

end

produces the error:

 *** Outer syntax error: exactly one command expected

[Makarius]

I usually use a proper command, such as "." or "done".

Anyway, the above error happens because the semicolon is included in the Isabelle.command span sent to the process, and that considers ";" as a second full command. This might be a bit picky, but it is how the published Isabelle releases do it.

[David Aspinall]

This is a nasty corner case, seems a bit minor since semi-colons are deprecated from proof scripts (aren't they?). But I understand the desire to step through comments in Isar.

Behind the scenes, the ";" is sent at the start of the second command, because it is explicitly added to the regexp which matches command starts. We could experiment with different settings for the command start regexp...

Should this work for all kinds of comments? Is it correct to have an empty command with a "--" type of comment?

[Makarius]

Interjections of the form -- TEXT can indeed occur everywhere within the input stream, so you can construct an empty command span that contains some of them. It all depends how you determine command spans, e.g. the Isabelle/Scala? layer attaches "--" to the adjacent command, to ensure that there is a proper context for antiquotations that can show up here.

Raw source comments of the (* ... *) are different, they can stand naked between commands, and need not be included in the span. On the other hand, these are not really comments how users expect them, and should hardly occur in proper Isar theory text. This is the story I keep telling for years, and many people still use (* ... *) instead of regular text {* ... *} nonetheless.

[Makarius]

The semicolon is not deprecated, but has practically come out of use in any user interface, except for the plain isabelle tty , where it is still needed.

I would give the issue of semicolons a very low priority in PG. Whenever I encounter spurious occurences in theory sources, I usually delete them on the spot.

[David Aspinall]

Moving this to next version to make a decision. Meanwhile (Lucas) you can always experiment with isar-any-command-regexp to tweak behaviour here.

Makarius, thanks for the useful remarks.

[David Aspinall]

Closing this, Lucas is moving a long way away so I should be safe from his wrath.