Opened 17 years ago
Last modified 11 years ago
#98 new defect
PGML changes: complete update for PGML 2.0
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
This will come from
- tokenised input (theory presentation)
- output display from pretty markup during display
In second case, need to re-tokenise a bit from Pretty.markup (strip whitespace prefix and suffix).
Note: output from pretty module needs to have token translation applied for print mode
(Output.output
). Should check this interacts well.
Change History (4)
comment:1 Changed 17 years ago by
Summary: | PGML change: add <whitespace> element → PGML changes: complete update for PGML 2.0 |
---|
comment:2 Changed 17 years ago by
Milestone: | PG-Eclipse-1.0.7 → PG-Eclipse-1.0.6 |
---|
comment:3 Changed 16 years ago by
Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
---|
comment:4 Changed 11 years ago by
Milestone: | PG-Eclipse-1.0.7 |
---|
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.0.7 deleted