src/Pure/ProofGeneral/ROOT.ML
author wenzelm
Thu, 20 Sep 2007 20:56:34 +0200
changeset 24666 9885a86f14a8
parent 24529 afd2be8a9aba
child 25223 7463251e7273
permissions -rw-r--r--
tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21943
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     1
(*  Title:      Pure/ProofGeneral/ROOT.ML
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     2
    ID:         $Id$
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     3
    Author:     David Aspinall
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     4
24529
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
     5
Proof General interface for Isabelle, both the traditional Emacs version,
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
     6
and PGIP experiments.
21943
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     7
*)
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     8
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
use "pgip_types.ML";
23610
5ade06703b07 Produce good PGML 2.0
aspinall
parents: 23570
diff changeset
    10
use "pgml.ML";
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    11
use "pgip_markup.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
use "pgip_input.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    13
use "pgip_output.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    14
use "pgip.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    16
use "pgip_isabelle.ML";
23610
5ade06703b07 Produce good PGML 2.0
aspinall
parents: 23570
diff changeset
    17
use "pgml_isabelle.ML";
24529
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
    18
(use |> setmp proofs 1 |> setmp quick_and_dirty true) "preferences.ML";
23793
b04afc51914c added ProofGeneral/pgip_parser.ML;
wenzelm
parents: 23610
diff changeset
    19
use "pgip_parser.ML";
b04afc51914c added ProofGeneral/pgip_parser.ML;
wenzelm
parents: 23610
diff changeset
    20
b04afc51914c added ProofGeneral/pgip_parser.ML;
wenzelm
parents: 23610
diff changeset
    21
use "parsing.ML";   (* old version *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    22
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    23
use "pgip_tests.ML";
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    24
24529
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
    25
use "proof_general_pgip.ML";
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
    26
use "proof_general_emacs.ML";
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    27