21997
|
1 |
(* Title: Pure/ProofGeneral/pgip_standalone.ML
|
21974
|
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 |
|
21997
|
14 |
(* The required parts of Isabelle libraries *)
|
21974
|
15 |
|
|
16 |
use "General/basics.ML";
|
|
17 |
use "library.ML";
|
|
18 |
use "General/position.ML";
|
|
19 |
use "General/path.ML"; (* used directly *)
|
|
20 |
use "General/table.ML";
|
|
21 |
use "General/alist.ML";
|
22589
|
22 |
|
|
23 |
val print_mode = ref ([]: string list);
|
|
24 |
fun print_mode_active s = member (op =) (! print_mode) s;
|
|
25 |
|
21974
|
26 |
use "General/output.ML";
|
|
27 |
use "General/scan.ML";
|
|
28 |
use "General/source.ML";
|
|
29 |
use "General/file.ML"; (* used directly *)
|
|
30 |
use "General/buffer.ML";
|
21997
|
31 |
use "General/symbol.ML";
|
21974
|
32 |
use "General/xml.ML"; (* used directly *)
|
|
33 |
use "General/url.ML"; (* used directly *)
|
|
34 |
|
|
35 |
|
21997
|
36 |
(* Our code *)
|
21974
|
37 |
|
21997
|
38 |
use "ProofGeneral/pgip_types.ML";
|
|
39 |
use "ProofGeneral/pgip_markup.ML";
|
|
40 |
use "ProofGeneral/pgip_input.ML";
|
|
41 |
use "ProofGeneral/pgip_output.ML";
|
|
42 |
use "ProofGeneral/pgip.ML";
|