Parsing Failure at ends of files

[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

[Graham Dutton]

this fixes the bug but creates another.

[Graham Dutton]

After much investigation, I'm now convinced that attached fix is the right thing, but it results in Processed region being set to '0' when the last line of the document is parsed. Investigating.