--- a/src/Pure/ProofGeneral/README Mon Jan 22 15:34:15 2007 +0100
+++ b/src/Pure/ProofGeneral/README Mon Jan 22 15:36:58 2007 +0100
@@ -14,19 +14,19 @@
The code constructs some marshalling datatypes for reading and writing
XML which conforms to the PGIP schema, interfacing with SML types and
some basic types from the Isabelle platform (i.e. URLs, XML). This
-part of the code is intended to be useful for reuse or porting
-elsewhere, so it should have minimal dependency on Isabelle and be
-written readably. Some languages have tools for making type-safe
-XML<->native datatype translations from a schema (e.g. HaXML for
-Haskell) which would be useful here.
+portion is intended to be useful for reuse or porting elsewhere, so it
+should have minimal dependency on Isabelle and be written readably.
+Some languages have tools for making type-safe XML<->native datatype
+translations from a schema (e.g. HaXML for Haskell) which would be
+useful here.
The Isabelle specific configuration is in these files:
- pgip_isabelle.ML - configure part of PGIP supported by Isabelle
- parsing.ML - parsing routines to add PGIP markup to scripts
- preferences.ML - user preferences
- proof_general_pgip.ML - the main connection point with Isabelle, including
- the PGIP processing loop.
+ pgip_isabelle.ML - configure part of PGIP supported by Isabelle + type mapping
+ parsing.ML - parsing routines to add PGIP markup to scripts
+ preferences.ML - user preferences
+ proof_general_pgip.ML - the main connection point with Isabelle, including
+ the PGIP processing loop.
For the full PGIP schema and an explanation of it, see: