Opened 13 years ago

Last modified 12 years ago

#425 accepted task

Consider simplifying span amalgamation to match prover undo behaviour

Reported by: David Aspinall Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc:

Description

With more flexible undo behaviour (e.g. linear undo in Isabelle), we can retire the old Goal...Save amalgamation. The remaining use seems really to be supporting outlining/folding, which would be better done by pattern matching and without adding additional confusing highlighting to the script.

Change History (1)

comment:1 Changed 12 years ago by David Aspinall

Milestone: PG-Emacs-4.2PG-Emacs-4.3
Status: newaccepted
Note: See TracTickets for help on using tickets.