21974
|
1 |
(* Title: Pure/ProofGeneral/pgip.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: David Aspinall
|
|
4 |
|
|
5 |
This file allows a standalone build of the PGIP abstraction module.
|
|
6 |
|
|
7 |
This should be useful for building other tools, or as an aid to porting.
|
|
8 |
|
|
9 |
A lot of Isabelle library code is pulled in, but only a few
|
|
10 |
functions are actually used, and the libraries indicated "used
|
|
11 |
directly" below could be replaced with other implementations.
|
|
12 |
|
|
13 |
NB: This is *not* part of the Isabelle build. As such, it's
|
|
14 |
liable to breakage as library functions are changed or moved around.
|
|
15 |
*)
|
|
16 |
|
|
17 |
val cd = OS.FileSys.chDir;
|
|
18 |
cd "..";
|
|
19 |
|
|
20 |
(* First you have to setup for your ML compiler.
|
|
21 |
This even requires extracting a function from the bash scripts!
|
|
22 |
See lib/scripts/run-XXX. This is for polyML 4.2.0.
|
|
23 |
*)
|
|
24 |
fun exit 0 = (OS.Process.exit OS.Process.success): unit
|
|
25 |
| exit _ = OS.Process.exit OS.Process.failure;
|
|
26 |
use "ML-Systems/polyml-4.2.0.ML";
|
|
27 |
|
|
28 |
(* Now the required parts of Isabelle libraries *)
|
|
29 |
|
|
30 |
use "General/basics.ML";
|
|
31 |
use "library.ML";
|
|
32 |
use "General/position.ML";
|
|
33 |
use "General/path.ML"; (* used directly *)
|
|
34 |
use "General/table.ML";
|
|
35 |
use "General/alist.ML";
|
|
36 |
use "General/output.ML";
|
|
37 |
use "General/scan.ML";
|
|
38 |
use "General/source.ML";
|
|
39 |
use "General/file.ML"; (* used directly *)
|
|
40 |
use "General/buffer.ML";
|
|
41 |
use "General/symbol.ML";
|
|
42 |
use "General/xml.ML"; (* used directly *)
|
|
43 |
use "General/url.ML"; (* used directly *)
|
|
44 |
|
|
45 |
cd "ProofGeneral/";
|
|
46 |
|
|
47 |
use "syntax_standalone.ML";
|
|
48 |
|
|
49 |
(* Finally, our code *)
|
|
50 |
|
|
51 |
use "pgip_types.ML";
|
|
52 |
use "pgip_markup.ML";
|
|
53 |
use "pgip_input.ML";
|
|
54 |
use "pgip_output.ML";
|
|
55 |
use "pgip.ML";
|