PGIP2 Roadmap

On this webpage we describe a roadmap how to smoothly move from the current PGKit implementation towards integrating the new features and concepts of PGIP2.

1. Change the internal PGIP markup to the new, tree-structured markup of PGIP2 and write the appropriate converters to go back and forth between the old and the new PGIP specific markup. Invariant: the current/old interfaces to Isabelle/HOL and Emacs should still work after the operation.
2. Move from the current interface protocol to XUPDATE and allow to integrate modifications from the prover as well.
3. Implement the multiple foci mechanism in PGKit
4. Move to support multiple displays (also provers?) simultanously by implementing the repository-like behaviour in the server.
5. Relay service requests context-sensitively from displays to provers and menus in the back direction. Allow patches from the prover to affect open menus as well.
6. Build the transformator that mediates between oldish ASCII formats of provers and XML-representation, e.g. OMDOC.

Any comments/suggestions are welcome.

-- SergeAutexier - 19 Jun 2008