Parsing Failure on TestLcl.thy

[Graham Dutton]

Parsing a file with no trailing whitespace fails.

For example: TestLcl.thy in test repository fails at the final lines. PG parses the final two lines:

 end
end

as a single unit:

 end[newline]en

(where [newline] is an actual newline), discarding the final character.

A functionally identical file TestLocale.thy with trailing whitespace will not exhibit this behaviour.

[Graham Dutton]

This of course results in broken prover interaction:

PGIP:

<pgip tag="PG-Eclipse" class="pa" id="/grape//6129632130384117" seq="107"><closetheory>end
en</closetheory></pgip>

Response:

Outer syntax error: command expected,
but identifier en was found

[Graham Dutton]

Actually appears to be an out-by-one error: can recreate on any thy file by trimming all trailing whitespace.

[Graham Dutton]

a partial solution: the line in question