renamed Isar/isar_output.ML to Thy/thy_output.ML;
renamed Isar/term_style.ML to Thy/term_style.ML;
renamed Isar/thy_header.ML to Thy/thy_header.ML;
added Isar/spec_parse.ML;
added Thy/ml_context.ML;
load outer_parse.ML early, moved later parts to spec_parse.ML;
tuned order;
--- a/src/Pure/Isar/ROOT.ML Fri Jan 19 22:08:21 2007 +0100
+++ b/src/Pure/Isar/ROOT.ML Fri Jan 19 22:08:22 2007 +0100
@@ -13,7 +13,17 @@
use "proof_context.ML";
use "local_defs.ML";
-(*theory presentation*)
+(*outer syntax*)
+use "outer_lex.ML";
+use "args.ML";
+use "outer_parse.ML";
+use "outer_keyword.ML";
+use "antiquote.ML";
+
+(*theory sources*)
+use "../Thy/ml_context.ML";
+use "../Thy/thy_load.ML";
+use "../Thy/thy_info.ML";
use "../Thy/html.ML";
use "../Thy/latex.ML";
use "../Thy/present.ML";
@@ -22,7 +32,6 @@
(*basic proof engine*)
use "proof_display.ML";
-use "args.ML";
use "attrib.ML";
use "context_rules.ML";
use "skip_proof.ML";
@@ -37,26 +46,22 @@
use "calculation.ML";
use "obtain.ML";
use "locale.ML";
+use "spec_parse.ML";
use "../axclass.ML";
use "theory_target.ML";
use "specification.ML";
use "constdefs.ML";
-(*outer syntax*)
-use "antiquote.ML";
-use "outer_parse.ML";
-use "outer_keyword.ML";
-
(*toplevel environment*)
use "proof_history.ML";
use "toplevel.ML";
(*theory presentation*)
-use "term_style.ML";
-use "isar_output.ML";
+use "../Thy/term_style.ML";
+use "../Thy/thy_output.ML";
(*theory syntax*)
-use "thy_header.ML";
+use "../Thy/thy_header.ML";
use "session.ML";
use "../old_goals.ML";
use "outer_syntax.ML";