1.1 --- a/src/Pure/ProofGeneral/README	Mon May 13 21:03:30 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,37 +0,0 @@
     1.4 -Proof General interface for Isabelle.
     1.5 -
     1.6 -This includes a prover-side PGIP abstraction layer for passing
     1.7 -interface configuration, control commands and display messages to
     1.8 -Proof General.
     1.9 -
    1.10 -  pgip_types.ML    -- the datatypes in PGIP and their manipulation
    1.11 -  pgip_input.ML	   -- commands sent to the prover
    1.12 -  pgip_output.ML   -- commands the prover sends out
    1.13 -  pgip_markup.ML   -- markup for proof script documents
    1.14 -  pgip.ML	   -- union of the above
    1.15 -  pgip_tests.ML    -- some basic testing of the API
    1.16 -
    1.17 -The code constructs some marshalling datatypes for reading and writing
    1.18 -XML which conforms to the PGIP schema, interfacing with SML types and
    1.19 -some basic types from the Isabelle platform (i.e. URLs, XML).  This
    1.20 -portion is intended to be useful for reuse or porting elsewhere, so it
    1.21 -should have minimal dependency on Isabelle and be written readably.
    1.22 -Some languages have tools for making type-safe XML<->native datatype
    1.23 -translations from a schema (e.g. HaXML for Haskell) which would be
    1.24 -useful here.
    1.25 -
    1.26 -The Isabelle specific configuration is in these files:
    1.27 -
    1.28 -  pgip_isabelle.ML	 - configure part of PGIP supported by Isabelle + type mapping
    1.29 -  parsing.ML		 - parsing routines to add PGIP markup to scripts
    1.30 -  preferences.ML	 - user preferences
    1.31 -  proof_general_pgip.ML  - the main connection point with Isabelle, including
    1.32 -			   the PGIP processing loop.
    1.33 -
    1.34 -For the full PGIP schema and an explanation of it, see:
    1.35 -
    1.36 -   http://proofgeneral.inf.ed.ac.uk/kit
    1.37 -   http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP
    1.38 -
    1.39 -David Aspinall, Dec. 2006.
    1.40 -