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.
- 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.
- Move from the current interface protocol to XUPDATE and allow to integrate modifications from the prover as well.
- Implement the multiple foci mechanism in PGKit
- Move to support multiple displays (also provers?) simultanously by implementing the repository-like behaviour in the server.
- 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.
- 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