|
1 Proof General interface for Isabelle. |
|
2 |
|
3 This includes a prover-side PGIP abstraction layer for passing |
|
4 interface configuration, control commands and display messages to |
|
5 Proof General. |
|
6 |
|
7 pgip_types.ML -- the datatypes in PGIP and their manipulation |
|
8 pgip_input.ML -- commands sent to the prover |
|
9 pgip_output.ML -- commands the prover sends out |
|
10 pgip_markup.ML -- markup for proof script documents |
|
11 pgip.ML -- union of the above |
|
12 pgip_tests.ML -- some basic testing of the API |
|
13 |
|
14 The code constructs some marshalling datatypes for reading and writing |
|
15 XML which conforms to the PGIP schema, interfacing with SML types and |
|
16 some basic types from the Isabelle platform (i.e. URLs, XML). This |
|
17 part of the code is intended to be useful for reuse or porting |
|
18 elsewhere, so it should have minimal dependency on Isabelle and be |
|
19 written readably. Some languages have tools for making type-safe |
|
20 XML<->native datatype translations from a schema (e.g. HaXML for |
|
21 Haskell) which would be useful here. |
|
22 |
|
23 The Isabelle specific configuration is in these files: |
|
24 |
|
25 pgip_isabelle.ML - configure part of PGIP supported by Isabelle |
|
26 parsing.ML - parsing routines to add PGIP markup to scripts |
|
27 preferences.ML - user preferences |
|
28 proof_general_pgip.ML - the main connection point with Isabelle, including |
|
29 the PGIP processing loop. |
|
30 |
|
31 For the full PGIP schema and an explanation of it, see: |
|
32 |
|
33 http://proofgeneral.inf.ed.ac.uk/kit |
|
34 |
|
35 David Aspinall, Dec. 2006. |
|
36 $Id$ |