Opened 16 years ago
Last modified 11 years ago
#243 new defect
Parsing errors: whitespace lost in parseresult
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description
Parser.java needs more cleanup: whitespace is being lost, and the recursive method calls are causing overflows when matching fails. The default assumption should be for correct matching, and we should fit with the parser in Isabelle2008 now (even though that is not quite right).
Change History (2)
comment:1 Changed 16 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
|---|---|
| Priority: | blocker → major |
Note: See
TracTickets for help on using
tickets.
Whitespace problem isolated in SessionManager? where system-dependent line end is added to lines of input (StringManipulation?.lineend) with some faulty heuristics. Replaced with single unix CR for now, so good enough for 1.0.6 linux release only. But should review behaviour on other OSes for next release.