1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 08 20:27:09 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 08 21:44:47 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  signature OUTER_SYNTAX =
     1.5  sig
     1.6    type outer_syntax
     1.7 +  val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
     1.8    val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
     1.9    val command: string -> string -> Keyword.T ->
    1.10      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.11 @@ -33,8 +34,10 @@
    1.12    val process_file: Path.T -> theory -> theory
    1.13    type isar
    1.14    val isar: TextIO.instream -> bool -> isar
    1.15 +  val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
    1.16 +  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
    1.17 +    (Toplevel.transition * Toplevel.transition list) list
    1.18    val prepare_command: Position.T -> string -> Toplevel.transition
    1.19 -  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future
    1.20  end;
    1.21  
    1.22  structure Outer_Syntax: OUTER_SYNTAX =
    1.23 @@ -283,41 +286,5 @@
    1.24      | _ => Toplevel.malformed pos not_singleton)
    1.25    end;
    1.26  
    1.27 -
    1.28 -(* load_thy *)
    1.29 -
    1.30 -fun load_thy name init pos text =
    1.31 -  let
    1.32 -    val (lexs, outer_syntax) = get_syntax ();
    1.33 -    val time = ! Toplevel.timing;
    1.34 -
    1.35 -    val _ = Present.init_theory name;
    1.36 -
    1.37 -    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
    1.38 -    val spans = Source.exhaust (Thy_Syntax.span_source toks);
    1.39 -    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
    1.40 -    val elements =
    1.41 -      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
    1.42 -      |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element outer_syntax init)
    1.43 -      |> flat;
    1.44 -
    1.45 -    val _ = Present.theory_source name
    1.46 -      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    1.47 -
    1.48 -    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    1.49 -    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
    1.50 -    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    1.51 -
    1.52 -    val present =
    1.53 -      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
    1.54 -        deps = map Future.task_of results, pri = 0})
    1.55 -      (fn () =>
    1.56 -        Thy_Output.present_thy (#1 lexs) Keyword.command_tags (is_markup outer_syntax)
    1.57 -          (maps Future.join results) toks
    1.58 -        |> Buffer.content
    1.59 -        |> Present.theory_output name);
    1.60 -
    1.61 -  in (thy, present) end;
    1.62 -
    1.63  end;
    1.64  

     2.1 --- a/src/Pure/ROOT.ML	Fri Jul 08 20:27:09 2011 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Fri Jul 08 21:44:47 2011 +0200
     2.3 @@ -243,18 +243,18 @@
     2.4  use "Isar/typedecl.ML";
     2.5  
     2.6  (*toplevel transactions*)
     2.7 -use "Thy/thy_load.ML";
     2.8  use "Isar/proof_node.ML";
     2.9  use "Isar/toplevel.ML";
    2.10  
    2.11  (*theory documents*)
    2.12  use "System/isabelle_system.ML";
    2.13 -use "Thy/present.ML";
    2.14  use "Thy/term_style.ML";
    2.15  use "Thy/thy_output.ML";
    2.16  use "Thy/thy_syntax.ML";
    2.17  use "Isar/outer_syntax.ML";
    2.18  use "PIDE/document.ML";
    2.19 +use "Thy/present.ML";
    2.20 +use "Thy/thy_load.ML";
    2.21  use "Thy/thy_info.ML";
    2.22  use "Thy/rail.ML";
    2.23  

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

     4.1 --- a/src/Pure/Thy/thy_info.ML	Fri Jul 08 20:27:09 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Jul 08 21:44:47 2011 +0200
     4.3 @@ -241,7 +241,7 @@
     4.4  fun required_by _ [] = ""
     4.5    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
     4.6  
     4.7 -fun load_thy initiators update_time deps text name parent_thys =
     4.8 +fun load_thy initiators update_time deps text name parents =
     4.9    let
    4.10      val _ = kill_thy name;
    4.11      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
    4.12 @@ -250,11 +250,8 @@
    4.13      val dir = Path.dir thy_path;
    4.14      val pos = Path.position thy_path;
    4.15      val (_, _, uses) = Thy_Header.read pos text;
    4.16 -    fun init _ =
    4.17 -      Thy_Load.begin_theory dir name imports parent_thys uses
    4.18 -      |> Present.begin_theory update_time dir uses;
    4.19  
    4.20 -    val (theory, present) = Outer_Syntax.load_thy name init pos text;
    4.21 +    val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents;
    4.22      fun commit () = update_thy deps theory;
    4.23    in (theory, present, commit) end;
    4.24  
    4.25 @@ -332,8 +329,8 @@
    4.26      val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
    4.27      val _ = kill_thy name;
    4.28      val _ = use_thys_wrt dir imports;
    4.29 -    val parent_thys = map (get_theory o base_name) imports;
    4.30 -  in Thy_Load.begin_theory dir name imports parent_thys uses end;
    4.31 +    val parents = map (get_theory o base_name) imports;
    4.32 +  in Thy_Load.begin_theory dir name imports uses parents end;
    4.33  
    4.34  
    4.35  (* register theory *)

     5.1 --- a/src/Pure/Thy/thy_load.ML	Fri Jul 08 20:27:09 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Jul 08 21:44:47 2011 +0200
     5.3 @@ -18,7 +18,10 @@
     5.4    val all_current: theory -> bool
     5.5    val use_ml: Path.T -> unit
     5.6    val exec_ml: Path.T -> generic_theory -> generic_theory
     5.7 -  val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
     5.8 +  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list ->
     5.9 +    theory list -> theory
    5.10 +  val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list ->
    5.11 +    Position.T -> string -> theory list -> theory * unit future
    5.12    val set_master_path: Path.T -> unit
    5.13    val get_master_path: unit -> Path.T
    5.14  end;
    5.15 @@ -149,15 +152,53 @@
    5.16  fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
    5.17  
    5.18  
    5.19 -(* begin theory *)
    5.20 +(* load_thy *)
    5.21  
    5.22 -fun begin_theory dir name imports parents uses =
    5.23 +fun begin_theory dir name imports uses parents =
    5.24    Theory.begin_theory name parents
    5.25    |> put_deps dir imports
    5.26    |> fold (require o fst) uses
    5.27    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
    5.28    |> Theory.checkpoint;
    5.29  
    5.30 +fun load_thy update_time dir name imports uses pos text parents =
    5.31 +  let
    5.32 +    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
    5.33 +    val time = ! Toplevel.timing;
    5.34 +
    5.35 +    val _ = Present.init_theory name;
    5.36 +    fun init _ =
    5.37 +      begin_theory dir name imports uses parents
    5.38 +      |> Present.begin_theory update_time dir uses;
    5.39 +
    5.40 +    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
    5.41 +    val spans = Source.exhaust (Thy_Syntax.span_source toks);
    5.42 +    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
    5.43 +    val elements =
    5.44 +      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
    5.45 +      |> Par_List.map_name "Outer_Syntax.prepare_element"
    5.46 +        (Outer_Syntax.prepare_element outer_syntax init)
    5.47 +      |> flat;
    5.48 +
    5.49 +    val _ = Present.theory_source name
    5.50 +      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    5.51 +
    5.52 +    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    5.53 +    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
    5.54 +    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    5.55 +
    5.56 +    val present =
    5.57 +      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
    5.58 +        deps = map Future.task_of results, pri = 0})
    5.59 +      (fn () =>
    5.60 +        Thy_Output.present_thy (#1 lexs) Keyword.command_tags
    5.61 +          (Outer_Syntax.is_markup outer_syntax)
    5.62 +          (maps Future.join results) toks
    5.63 +        |> Buffer.content
    5.64 +        |> Present.theory_output name);
    5.65 +
    5.66 +  in (thy, present) end;
    5.67 +
    5.68  
    5.69  (* global master path *)
    5.70