Opened 17 years ago
Last modified 11 years ago
#142 new defect
New parsescript code in pgip_parser.ML is broken
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 4:prover-isabelle | Keywords: | |
| Cc: |
Description
We must fix the double escaping of XML before the new parsing code can be used.
Change History (4)
comment:1 Changed 17 years ago by
| Milestone: | PG-Emacs-3.7 → PG-Eclipse-1.0.6 |
|---|
comment:2 Changed 17 years ago by
comment:3 Changed 16 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
|---|
Unfortunately this may still be a problem in Isabelle2008, I think I have seen simplifier output which is not correctly escaped and confuses the XML input stream. Very unfortunate. Example needed. Input file parsing seems reliable however.
Pushing milestone. Any future release should fix this.
Note: See
TracTickets for help on using
tickets.
Note: see #83 for previous notes about PGIP parsing requirements.