Opened 17 years ago

Last modified 11 years ago

#44 new enhancement

Support openblock/closeblock elements in prover parse output.

Reported by: David Aspinall <da+pgtrac@…> 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

Change History (1)

comment:1 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0

Milestone PG-Eclipse-1.1.0 deleted

Note: See TracTickets for help on using tickets.