Proof General Kit Development Issues
Notes on the development of
ProofGeneralKit. See also
PGIPDevelNotes.
Issues
An issue is a bug which has not yet become a feature. We have the following:
- Performance of parsing was an issue, but the broker is now fast enough with XML handling to make Isabelle the problem. That has now been repaired, too.
- When a display opens a file a second time, broker reports
"file already open"
. (A problem when reopening a buffer after killing it in PGEmacs.)
- The
<restartprover>
display message does not work yet. See this discussion.
- When an atom is deleted, its children will need to find a new parent, namely the parent of the deleted atom (if it exists). Currently, displays have to figure that out. It would be good if the broker could do that for them, but that would need a new display message which informs displays about changes in the parent structure.
Once an Issue has been identified as a bug or a feature, and resolved, it goes on the list of
ProofGeneralResolvedIssues .
Request for Changes
This section is to discuss changes to the broker, or
PGIP, which are more than just bug-fixes, and may break compatibility to other components (should not be done light-heartedly of course). These may result from the Issues above or discussions below.
Development Discussions
Just a list of points that we thought about, or should think about.
Main.KitDevelIssues moved from Main.ProofGeneralIssues on 27 Sep 2006 - 10:52 by DavidAspinall