#248 closed (fixed)
Clear error markers at correct points (e.g., when processing text successfully)
Reported by: | David Aspinall | Owned by: | Graham Dutton |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
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).
Change History (3)
comment:1 Changed 16 years ago by
Owner: | changed from David Aspinall to Graham Dutton |
---|
comment:2 Changed 16 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Fixed in ProofScriptDocument? 1.120