Opened 17 years ago
Last modified 11 years ago
#97 new defect
Add Pretty.markup to parse tree output
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | 4:prover-isabelle | Keywords: | |
| Cc: |
Description
This will allow several things:
- Markup on constants as well as variables, e.g. for colouring
- Query to discover type: although only most general type by lookup in theory (not from term)
- This will enable (e.g., hyperlinked) references to be given to locate definitions.
See printer.ML.
Makarius will pass through additional token translation functions for constants and pieces of mixfix.
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted