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.

[David Aspinall]

Sounds like a separate problem since files without final CR were not being parsed before.

My diff corrects the termination check at the end of the loop (notice that real error was in calculation of length=endOffset-startOffset, which should be endOffset-startOffset+1).

[Graham Dutton]

Yes, that is much more complete fix, and means that the fix I was working on for the subsequent issue now actually works... Commit on its way.

[Graham Dutton]

appears to be fixed.

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted