--- a/src/Pure/ProofGeneral/README Mon May 13 21:03:30 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-Proof General interface for Isabelle.
-
-This includes a prover-side PGIP abstraction layer for passing
-interface configuration, control commands and display messages to
-Proof General.
-
- pgip_types.ML -- the datatypes in PGIP and their manipulation
- pgip_input.ML -- commands sent to the prover
- pgip_output.ML -- commands the prover sends out
- pgip_markup.ML -- markup for proof script documents
- pgip.ML -- union of the above
- pgip_tests.ML -- some basic testing of the API
-
-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
-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 + 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:
-
- http://proofgeneral.inf.ed.ac.uk/kit
- http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP
-
-David Aspinall, Dec. 2006.
-