Publikation
Towards Merging Plato and PGIP
David Aspinall; Serge Autexier; Christoph Lüth; Marc Wagner
In: Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers. Workshop on User Interfaces for Theorem Provers (UITP-2008), August 22, Montreal, QC, Canada, Pages 3-21, Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 226, Elsevier Science, 2009.
Zusammenfassung
The PGIP protocol is a standard, abstract interface protocol to connect theorem provers with user interfaces. Interaction in PGIP is based on ASCII-text input and a single focus point-of-control, which indicates a linear position in the input that has been checked thus far. This fits many interactive theorem provers whose interaction model stems from command-line interpreters. Plato, on the other hand, is a system with a new protocol tailored to transparently integrate theorem provers into text editors like TEXmacs that support semi-structured XML input files and multiple foci of attention. In this paper we extend the PGIP protocol and middleware broker to support the functionalities provided by Plato and beyond. More specifically, we extend PGIP (i) to support multiple foci in provers; (ii) to display semi-structured documents; (iii) to combine prover updates with user edits; (iv) to support context-sensitive service menus, and (v) to allow multiple displays. As well as supporting TEXmacs, the extended PGIP protocol in principle can support other editors such as OpenOffice, Word 2007 and graph viewers; we hope it will also provide guidance for extending provers to handle multiple foci.