src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Apr 18 16:34:58 2017 +0200
@@ -18,6 +18,7 @@
   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 ->
@@ -29,10 +30,6 @@
   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 =
@@ -101,7 +98,10 @@
 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 *)
@@ -199,67 +199,6 @@
       | 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