Opened 14 years ago
Closed 14 years ago
#344 closed defect (fixed)
proof-retract-buffer incomplete
| Reported by: | Makarius | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | makarius@… |
Description
proof-retract-buffer fails to retract to the start of the theory, if there is any non-command material before the header, e.g. a comment.
Example:
(*blah*) theory A imports Main begin
assert -- retract-buffer -- sync lost
BTW, it should be safe to issue the magic sequence init_toplevel; kill_thy A unconditionally, even if that theory has never really been started.
Change History (2)
comment:1 Changed 14 years ago by
| Cc: | makarius@… added |
|---|
comment:2 Changed 14 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Thanks. A bug with nested spans and the find-forget loop. This was case I lost for #335.