Opened 17 years ago

Closed 17 years ago

Last modified 11 years ago

#6 closed enhancement (fixed)

Add code folding for proof scripts

Reported by: anonymous Owned by: David Aspinall
Priority: major Milestone:
Component: 1:pg-eclipse Keywords:
Cc:

Description

Add code folding for proof scripts. Hua Yang had some experimental code which hard-coded Isabelle syntax; this should be revisited and revised to use the document parse instead.

Change History (3)

comment:1 Changed 17 years ago by David Aspinall

Priority: minor → major

comment:2 Changed 17 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Good basic support for code folding has now been added. It is enabled by turning on the preference in the Miscellaneous panel. It is labelled as experimental because the implementation is inefficient at present. Desirable improvements:

  • Efficiency improvement
  • Tweaks to e.g. extract captions from comments which have otherwise empty first line. This can be done by scanning for comment prefixes, skipping whitespace.
  • Harmonisation with script management actions: currently Next action sometimes leaves regions folded, sometimes not. Could automatically skip over folded sections with assumption that user does not want to see proof inside them.

Closing for now as fixed, will unfold again later...

comment:3 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.6

Milestone PG-Eclipse-1.0.6 deleted

Note: See TracTickets for help on using tickets.