Custom Query (361 matches)

At the moment error markers are only removed when text is edited or reparsed. But it is possible to repair an error without changing the text locally: for example,

theory ErrorMarkerCleaning imports Main NewTheory
begin

end

Process this without then with NewTheory?.thy being present in the directory (see test case in ed.inf.proofgeneral.tests project).

this was created without email verification.

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.