src/Pure/ProofGeneral/README
author wenzelm
Mon Mar 02 20:29:43 2009 +0100 (2009-03-02)
changeset 30204 8ede2f7104cf
parent 22160 27cdecde8c2b
permissions -rw-r--r--
removed Ids;
     1 Proof General interface for Isabelle.
     2 
     3 This includes a prover-side PGIP abstraction layer for passing
     4 interface configuration, control commands and display messages to
     5 Proof General.
     6 
     7   pgip_types.ML    -- the datatypes in PGIP and their manipulation
     8   pgip_input.ML	   -- commands sent to the prover
     9   pgip_output.ML   -- commands the prover sends out
    10   pgip_markup.ML   -- markup for proof script documents
    11   pgip.ML	   -- union of the above
    12   pgip_tests.ML    -- some basic testing of the API
    13 
    14 The code constructs some marshalling datatypes for reading and writing
    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
    17 portion is intended to be useful for reuse or porting elsewhere, so it
    18 should have minimal dependency on Isabelle and be written readably.
    19 Some languages have tools for making type-safe XML<->native datatype
    20 translations from a schema (e.g. HaXML for Haskell) which would be
    21 useful here.
    22 
    23 The Isabelle specific configuration is in these files:
    24 
    25   pgip_isabelle.ML	 - configure part of PGIP supported by Isabelle + type mapping
    26   parsing.ML		 - parsing routines to add PGIP markup to scripts
    27   preferences.ML	 - user preferences
    28   proof_general_pgip.ML  - the main connection point with Isabelle, including
    29 			   the PGIP processing loop.
    30 
    31 For the full PGIP schema and an explanation of it, see:
    32 
    33    http://proofgeneral.inf.ed.ac.uk/kit
    34    http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP
    35 
    36 David Aspinall, Dec. 2006.
    37