Parsing, editing, proving: The PGIP display protocol
David Aspinall, Christoph Lüth, Daniel Winterstein · 2005
This paper describes how proof texts are constructed and edited in the Proof Gen-eral Kit framework. Proof texts are the central object of development within our framework and we want to allow flexible ways to construct them, both explicitly via text editing and implicitly by graphical manipulation or meta-manipulation. To this end, the framework allows for user-oriented display components, connected to provers via a central broker component. The display components and the bro-ker exchange messages in a format specified by the PGIP display protocol, which facilitates parsing, editing and proving of proof texts. The design of this part of the framework is new; the remainder of the frame-work, which connects the prover components to the broker, is based more closely on refining work of the previous Proof General project, and was described in [4]. 1