src/Pure/PIDE/resources.ML

   val global_theory: string -> string option
   val loaded_theory: string -> string option
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
+  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->

     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   val parse_files: string -> (theory -> Token.file list) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
-  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
-    Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
-    theory * (unit -> unit) * int
 end;
 
 structure Resources: RESOURCES =
 struct
 

 
 
 val master_directory = #master_dir o Files.get;
 val imports_of = #imports o Files.get;
 
-fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
+fun begin_theory master_dir {name, imports, keywords} parents =
+  Theory.begin_theory name parents
+  |> map_files (fn _ => (master_dir, imports, []))
+  |> Thy_Header.add_keywords keywords;
 
 
 (* theory files *)
 
 val thy_path = Path.ext "thy";

   #provided (Files.get thy) |>
     forall (fn (src_path, id) =>
       (case try (load_file thy) src_path of
         NONE => false
       | SOME ((_, id'), _) => id = id'));
-
-
-(* load theory *)
-
-fun begin_theory master_dir {name, imports, keywords} parents =
-  Theory.begin_theory name parents
-  |> put_deps master_dir imports
-  |> Thy_Header.add_keywords keywords;
-
-fun excursion keywords master_dir last_timing init elements =
-  let
-    fun prepare_span st span =
-      Command_Span.content span
-      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
-      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
-
-    fun element_result span_elem (st, _) =
-      let
-        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
-        val (results, st') = Toplevel.element_result keywords elem st;
-        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
-      in (results, (st', pos')) end;
-
-    val (results, (end_state, end_pos)) =
-      fold_map element_result elements (Toplevel.toplevel, Position.none);
-
-    val thy = Toplevel.end_theory end_pos end_state;
-  in (results, thy) end;
-
-fun load_thy document symbols last_timing update_time master_dir header text_pos text parents =
-  let
-    val (name, _) = #name header;
-    val keywords =
-      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
-        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
-
-    val toks = Token.explode keywords text_pos text;
-    val spans = Outer_Syntax.parse_spans toks;
-    val elements = Thy_Syntax.parse_elements keywords spans;
-
-    fun init () =
-      begin_theory master_dir header parents
-      |> Present.begin_theory update_time
-        (fn () => implode (map (HTML.present_span symbols keywords) spans));
-
-    val (results, thy) =
-      cond_timeit true ("theory " ^ quote name)
-        (fn () => excursion keywords master_dir last_timing init elements);
-
-    fun present () =
-      let
-        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
-      in
-        if exists (Toplevel.is_skipped_proof o #2) res then
-          warning ("Cannot present theory with skipped proofs: " ^ quote name)
-        else
-          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
-          in if document then Present.theory_output (Long_Name.base_name name) tex_source else () end
-      end;
-
-  in (thy, present, size text) end;
 
 
 (* antiquotations *)
 
 local