Opened 11 years ago
#464 new defect
proof script not displayed after startup
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
(I'm Dan Grayson <dan@…>)
I'm adapting pg under emacs to a new proof assistant that I'm writing (see https://github.com/DanGrayson/checker), and have just gotten started. The first problem was that after pg started scripting my proof script, the proof script buffer would disappear about the same time the *goals* and *response* buffers were displayed. I tracked the problem down to the function proof-display-three-b receiving nil as its first argument (why, I don't know), and "fixed" it as in the attached patch.
Note: See
TracTickets for help on using
tickets.