#69 closed defect (fixed)
PGMarkerMethods: skip spaces in document before error marker start
| Reported by: | Owned by: | Graham Dutton | |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
If error marker has been set by us based on command from document, spaces should be skipped which, if present, appear before start of command text proper. Test case:
(* this is a comment *) lemma "!"
Change History (3)
comment:1 Changed 17 years ago by
| Description: | modified (diff) |
|---|---|
| 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.
This problem is no longer present with new parser/Isabelle2008.