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
Milestone: | PG-Emacs-4.2 → PG-Emacs-4.3 |
---|---|
Status: | new → accepted |
Note: See
TracTickets for help on using
tickets.