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 portion is intended to be useful for reuse or porting elsewhere, so it |
|
18 should have minimal dependency on Isabelle and be written readably. |
|
19 Some languages have tools for making type-safe XML<->native datatype |
|
20 translations from a schema (e.g. HaXML for Haskell) which would be |
|
21 useful here. |
|
22 |
|
23 The Isabelle specific configuration is in these files: |
|
24 |
|
25 pgip_isabelle.ML - configure part of PGIP supported by Isabelle + type mapping |
|
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 http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP |
|
35 |
|
36 David Aspinall, Dec. 2006. |
|
37 |
|