# HG changeset patch # User wenzelm # Date 1169240902 -3600 # Node ID 4a65d2f4d0b59ffb93e4025b9ebd59230cf37ce2 # Parent 6a90ac654c6d641d19777eb70dd0393e4a98be0d 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; diff -r 6a90ac654c6d -r 4a65d2f4d0b5 src/Pure/Isar/ROOT.ML --- 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";