Add standalone file to help porters
authoraspinall
Sun Dec 31 15:57:58 2006 +0100 (2006-12-31)
changeset 21974c4e4d34fbc60
parent 21973 e7c9b0d3ce82
child 21975 1152dc45d591
Add standalone file to help porters
src/Pure/ProofGeneral/pgip_standalone.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ProofGeneral/pgip_standalone.ML	Sun Dec 31 15:57:58 2006 +0100
     1.3 @@ -0,0 +1,55 @@
     1.4 +(*  Title:      Pure/ProofGeneral/pgip.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     David Aspinall
     1.7 +
     1.8 +   This file allows a standalone build of the PGIP abstraction module.
     1.9 +
    1.10 +   This should be useful for building other tools, or as an aid to porting.
    1.11 +
    1.12 +   A lot of Isabelle library code is pulled in, but only a few
    1.13 +   functions are actually used, and the libraries indicated "used
    1.14 +   directly" below could be replaced with other implementations.
    1.15 +
    1.16 +   NB: This is *not* part of the Isabelle build.  As such, it's
    1.17 +   liable to breakage as library functions are changed or moved around.
    1.18 +*)
    1.19 +
    1.20 +val cd = OS.FileSys.chDir;
    1.21 +cd ".."; 
    1.22 +
    1.23 +(* First you have to setup for your ML compiler.
    1.24 +   This even requires extracting a function from the bash scripts! 
    1.25 +   See lib/scripts/run-XXX.  This is for polyML 4.2.0. 
    1.26 +*)
    1.27 +fun exit 0 = (OS.Process.exit OS.Process.success): unit 
    1.28 +  | exit _ = OS.Process.exit OS.Process.failure;
    1.29 +use "ML-Systems/polyml-4.2.0.ML";
    1.30 +
    1.31 +(* Now the required parts of Isabelle libraries *)
    1.32 +
    1.33 +use "General/basics.ML";
    1.34 +use "library.ML";
    1.35 +use "General/position.ML";
    1.36 +use "General/path.ML";     (* used directly *)
    1.37 +use "General/table.ML";
    1.38 +use "General/alist.ML";
    1.39 +use "General/output.ML";
    1.40 +use "General/scan.ML";
    1.41 +use "General/source.ML";
    1.42 +use "General/file.ML";     (* used directly *)
    1.43 +use "General/buffer.ML";
    1.44 +use "General/symbol.ML";  
    1.45 +use "General/xml.ML";      (* used directly *)
    1.46 +use "General/url.ML";      (* used directly *)
    1.47 +
    1.48 +cd "ProofGeneral/";
    1.49 +
    1.50 +use "syntax_standalone.ML"; 
    1.51 +
    1.52 +(* Finally, our code *)
    1.53 +
    1.54 +use "pgip_types.ML";
    1.55 +use "pgip_markup.ML";
    1.56 +use "pgip_input.ML";
    1.57 +use "pgip_output.ML";
    1.58 +use "pgip.ML";