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.

• PGDisplayProverIds - Using ProverId for display messages
• PGNewObjMessages - reporting existing objects

Development Discussions

Just a list of points that we thought about, or should think about.

• PGFileHandling - File handling
• PGRollingBack - Rolling back changes
• PGModTicks - Buffer modification ticks
• PGRevertReload - Reverting changes and reloading files
• PGDynamicComponents - How do we deal with Isabelle's logic selection mechanism?
• PGDispObjectManagement - Can we make managing objects easier for displays?