Parsing whole file is costly; lazy "gathering" parser strategy is flawed

[David Aspinall <da+pgtrac@…>]

Currently, parsing parses the entire file, but this is annoying for long files as it can take a couple of seconds. The alternative lazy "gathering" strategy implemented (which parses more and more lines until a valid parse is found) is flawed, e.g. multiple constdefs only takes the first, subsequent ones don't parse (hunts to end of file, which is SLOW!). Another failure example is on lemmas with multiple statements:

   lemma "A ??? B ==> B ??? A"
         "C ??? A ==> A"

i.e.: if (R) (RS) and (T) are valid parses, RST is parsed as (R) then fail, instead of (RS)(T).

We could fix this simply by looking for tthe next command boundary (second PGIP command in parseresult), or end of text, whichever comes first. That's how the code has worked in Emacs for years.

[David Aspinall]

Milestone PG-Eclipse-1.0.7 deleted