12 pgip_tests.ML -- some basic testing of the API |
12 pgip_tests.ML -- some basic testing of the API |
13 |
13 |
14 The code constructs some marshalling datatypes for reading and writing |
14 The code constructs some marshalling datatypes for reading and writing |
15 XML which conforms to the PGIP schema, interfacing with SML types and |
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 |
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 |
17 portion is intended to be useful for reuse or porting elsewhere, so it |
18 elsewhere, so it should have minimal dependency on Isabelle and be |
18 should have minimal dependency on Isabelle and be written readably. |
19 written readably. Some languages have tools for making type-safe |
19 Some languages have tools for making type-safe XML<->native datatype |
20 XML<->native datatype translations from a schema (e.g. HaXML for |
20 translations from a schema (e.g. HaXML for Haskell) which would be |
21 Haskell) which would be useful here. |
21 useful here. |
22 |
22 |
23 The Isabelle specific configuration is in these files: |
23 The Isabelle specific configuration is in these files: |
24 |
24 |
25 pgip_isabelle.ML - configure part of PGIP supported by Isabelle |
25 pgip_isabelle.ML - configure part of PGIP supported by Isabelle + type mapping |
26 parsing.ML - parsing routines to add PGIP markup to scripts |
26 parsing.ML - parsing routines to add PGIP markup to scripts |
27 preferences.ML - user preferences |
27 preferences.ML - user preferences |
28 proof_general_pgip.ML - the main connection point with Isabelle, including |
28 proof_general_pgip.ML - the main connection point with Isabelle, including |
29 the PGIP processing loop. |
29 the PGIP processing loop. |
30 |
30 |
31 For the full PGIP schema and an explanation of it, see: |
31 For the full PGIP schema and an explanation of it, see: |
32 |
32 |
33 http://proofgeneral.inf.ed.ac.uk/kit |
33 http://proofgeneral.inf.ed.ac.uk/kit |
34 http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP |
34 http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP |