moved Outer_Syntax.load_thy to Thy_Load.load_thy;
tuned signatures;
tuned module dependencies;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 08 20:27:09 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 08 21:44:47 2011 +0200
@@ -10,6 +10,7 @@
 signature OUTER_SYNTAX =
 sig
   type outer_syntax
+  val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
   val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
   val command: string -> string -> Keyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
@@ -33,8 +34,10 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
+  val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
+  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
+    (Toplevel.transition * Toplevel.transition list) list
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -283,41 +286,5 @@
     | _ => Toplevel.malformed pos not_singleton)
   end;
 
-
-(* load_thy *)
-
-fun load_thy name init pos text =
-  let
-    val (lexs, outer_syntax) = get_syntax ();
-    val time = ! Toplevel.timing;
-
-    val _ = Present.init_theory name;
-
-    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
-    val spans = Source.exhaust (Thy_Syntax.span_source toks);
-    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
-    val elements =
-      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
-      |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element outer_syntax init)
-      |> flat;
-
-    val _ = Present.theory_source name
-      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
-
-    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
-    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
-
-    val present =
-      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
-        deps = map Future.task_of results, pri = 0})
-      (fn () =>
-        Thy_Output.present_thy (#1 lexs) Keyword.command_tags (is_markup outer_syntax)
-          (maps Future.join results) toks
-        |> Buffer.content
-        |> Present.theory_output name);
-
-  in (thy, present) end;
-
 end;
 

--- a/src/Pure/ROOT.ML	Fri Jul 08 20:27:09 2011 +0200
+++ b/src/Pure/ROOT.ML	Fri Jul 08 21:44:47 2011 +0200
@@ -243,18 +243,18 @@
 use "Isar/typedecl.ML";
 
 (*toplevel transactions*)
-use "Thy/thy_load.ML";
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
 (*theory documents*)
 use "System/isabelle_system.ML";
-use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
 use "Isar/outer_syntax.ML";
 use "PIDE/document.ML";
+use "Thy/present.ML";
+use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
 use "Thy/rail.ML";
 

--- a/src/Pure/Thy/present.ML	Fri Jul 08 20:27:09 2011 +0200
+++ b/src/Pure/Thy/present.ML	Fri Jul 08 21:44:47 2011 +0200
@@ -461,7 +461,7 @@
 
     val files_html = files |> map (fn (raw_path, loadit) =>
       let
-        val path = Thy_Load.check_file dir raw_path;
+        val path = File.check_file (File.full_path dir raw_path);
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,

--- a/src/Pure/Thy/thy_info.ML	Fri Jul 08 20:27:09 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Jul 08 21:44:47 2011 +0200
@@ -241,7 +241,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time deps text name parent_thys =
+fun load_thy initiators update_time deps text name parents =
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -250,11 +250,8 @@
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
     val (_, _, uses) = Thy_Header.read pos text;
-    fun init _ =
-      Thy_Load.begin_theory dir name imports parent_thys uses
-      |> Present.begin_theory update_time dir uses;
 
-    val (theory, present) = Outer_Syntax.load_thy name init pos text;
+    val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents;
     fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
 
@@ -332,8 +329,8 @@
     val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
-    val parent_thys = map (get_theory o base_name) imports;
-  in Thy_Load.begin_theory dir name imports parent_thys uses end;
+    val parents = map (get_theory o base_name) imports;
+  in Thy_Load.begin_theory dir name imports uses parents end;
 
 
 (* register theory *)

--- a/src/Pure/Thy/thy_load.ML	Fri Jul 08 20:27:09 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Fri Jul 08 21:44:47 2011 +0200
@@ -18,7 +18,10 @@
   val all_current: theory -> bool
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
-  val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
+  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list ->
+    theory list -> theory
+  val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list ->
+    Position.T -> string -> theory list -> theory * unit future
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
@@ -149,15 +152,53 @@
 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
 
 
-(* begin theory *)
+(* load_thy *)
 
-fun begin_theory dir name imports parents uses =
+fun begin_theory dir name imports uses parents =
   Theory.begin_theory name parents
   |> put_deps dir imports
   |> fold (require o fst) uses
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
+fun load_thy update_time dir name imports uses pos text parents =
+  let
+    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
+    val time = ! Toplevel.timing;
+
+    val _ = Present.init_theory name;
+    fun init _ =
+      begin_theory dir name imports uses parents
+      |> Present.begin_theory update_time dir uses;
+
+    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
+    val spans = Source.exhaust (Thy_Syntax.span_source toks);
+    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
+    val elements =
+      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
+      |> Par_List.map_name "Outer_Syntax.prepare_element"
+        (Outer_Syntax.prepare_element outer_syntax init)
+      |> flat;
+
+    val _ = Present.theory_source name
+      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
+
+    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
+    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
+    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
+
+    val present =
+      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
+        deps = map Future.task_of results, pri = 0})
+      (fn () =>
+        Thy_Output.present_thy (#1 lexs) Keyword.command_tags
+          (Outer_Syntax.is_markup outer_syntax)
+          (maps Future.join results) toks
+        |> Buffer.content
+        |> Present.theory_output name);
+
+  in (thy, present) end;
+
 
 (* global master path *)