Proof General Kit Development Issues

Notes on the development of ProofGeneralKit. See also PGIPDevelNotes.


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.

Topic revision: r6 - 04 Dec 2006 - 11:29:35 - DavidAspinall
Main.KitDevelIssues moved from Main.ProofGeneralIssues on 27 Sep 2006 - 10:52 by DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies