# HG changeset patch
# User wenzelm
# Date 1368472021 -7200
# Node ID b9b2db1e7a5ee7c34f24b9fc4b078c23b38ed31d
# Parent  43fbd02eb9d0d760ef40aa3f7282418efb91ca46
obsolete;

diff -r 43fbd02eb9d0 -r b9b2db1e7a5e src/Pure/ProofGeneral/README
--- 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.
-