Opened 14 years ago

Closed 14 years ago

#335 closed defect (worksforme)

Script management: old-style undo broken in Isar

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

Description

Script management loses sync when Isabelle -> Settings -> Use Linear Undo is disabled.

Seems to be partly to do with regexp matching, but also a fault in counting.

Change History (1)

comment:1 Changed 14 years ago by David Aspinall

Resolution: worksforme
Status: newclosed

Can't duplicate now, likely to do with changing undo mechanism during scripting. Added call to proof-deactivate-scripting when changing undo mechanism to encourage completing/emptying the buffer and give a warning if this isn't done.

Note: See TracTickets for help on using tickets.