Opened 17 years ago
Last modified 11 years ago
#44 new enhancement
Support openblock/closeblock elements in prover parse output.
Reported by: | Owned by: | David Aspinall | |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
The openblock/closeblock elements should allow us to remove Isabelle specifics from parsing code, also cleaning it up. Two ideas behind these elements:
- Explain document nesting structure to PG, used for indentation, folding, outlining, ...
- Indicate named holes in document which can be replaced in dialog with the prover
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted