#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