# HG changeset patch
# User wenzelm
# Date 1414786806 -3600
# Node ID 897f266c44b301cf656474705fabdcdd3fd8ca05
# Parent  1bb0ad7827b49d1ad68a7fc6388be68022c3b5e7
obsolete;

diff -r 1bb0ad7827b4 -r 897f266c44b3 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Oct 31 21:10:11 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Oct 31 21:20:06 2014 +0100
@@ -15,7 +15,6 @@
   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: theory -> Path.T list
   val loaded_files_current: theory -> bool
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
@@ -116,11 +115,6 @@
         NONE => false
       | SOME ((_, id'), _) => id = id'));
 
-(*Proof General legacy*)
-fun loaded_files thy =
-  let val {master_dir, provided, ...} = Files.get thy
-  in map (File.full_path master_dir o #1) provided end;
-
 
 (* load theory *)
 
diff -r 1bb0ad7827b4 -r 897f266c44b3 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:10:11 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:20:06 2014 +0100
@@ -14,7 +14,6 @@
   val get_theory: string -> theory
   val is_finished: string -> bool
   val master_directory: string -> Path.T
-  val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val use_theories:
@@ -126,12 +125,6 @@
 
 val get_imports = Resources.imports_of o get_theory;
 
-(*Proof General legacy*)
-fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
-  (case get_deps name of
-    NONE => []
-  | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
-
 
 
 (** thy operations **)