equal
deleted
inserted
replaced
1 (* Title: Pure/ProofGeneral/ROOT.ML |
1 (* Title: Pure/ProofGeneral/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David Aspinall |
3 Author: David Aspinall |
4 |
4 |
5 Proof General interface for Isabelle. |
5 Proof General interface for Isabelle, both the traditional Emacs version, |
|
6 and PGIP experiments. |
6 *) |
7 *) |
7 |
8 |
8 use "pgip_types.ML"; |
9 use "pgip_types.ML"; |
9 use "pgml.ML"; |
10 use "pgml.ML"; |
10 use "pgip_markup.ML"; |
11 use "pgip_markup.ML"; |
12 use "pgip_output.ML"; |
13 use "pgip_output.ML"; |
13 use "pgip.ML"; |
14 use "pgip.ML"; |
14 |
15 |
15 use "pgip_isabelle.ML"; |
16 use "pgip_isabelle.ML"; |
16 use "pgml_isabelle.ML"; |
17 use "pgml_isabelle.ML"; |
17 use "preferences.ML"; |
18 (use |> setmp proofs 1 |> setmp quick_and_dirty true) "preferences.ML"; |
18 use "pgip_parser.ML"; |
19 use "pgip_parser.ML"; |
19 |
20 |
20 use "parsing.ML"; (* old version *) |
21 use "parsing.ML"; (* old version *) |
21 |
22 |
22 use "pgip_tests.ML"; |
23 use "pgip_tests.ML"; |
23 |
24 |
24 (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_pgip.ML"; |
25 use "proof_general_pgip.ML"; |
25 (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML"; |
26 use "proof_general_emacs.ML"; |
26 |
27 |
27 (* desirable to have tests on UI connection: |
|
28 use "pgip_isabelle_tests.ML" |
|
29 *) |
|