obsolete;
authorwenzelm
Fri Oct 31 21:20:06 2014 +0100 (2014-10-31 ago)
changeset 58851897f266c44b3
parent 58850 1bb0ad7827b4
child 58852 621c052789b4
obsolete;
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 31 21:10:11 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Oct 31 21:20:06 2014 +0100
     1.3 @@ -15,7 +15,6 @@
     1.4    val parse_files: string -> (theory -> Token.file list) parser
     1.5    val provide: Path.T * SHA1.digest -> theory -> theory
     1.6    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     1.7 -  val loaded_files: theory -> Path.T list
     1.8    val loaded_files_current: theory -> bool
     1.9    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    1.10    val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
    1.11 @@ -116,11 +115,6 @@
    1.12          NONE => false
    1.13        | SOME ((_, id'), _) => id = id'));
    1.14  
    1.15 -(*Proof General legacy*)
    1.16 -fun loaded_files thy =
    1.17 -  let val {master_dir, provided, ...} = Files.get thy
    1.18 -  in map (File.full_path master_dir o #1) provided end;
    1.19 -
    1.20  
    1.21  (* load theory *)
    1.22  
     2.1 --- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:10:11 2014 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:20:06 2014 +0100
     2.3 @@ -14,7 +14,6 @@
     2.4    val get_theory: string -> theory
     2.5    val is_finished: string -> bool
     2.6    val master_directory: string -> Path.T
     2.7 -  val loaded_files: string -> Path.T list
     2.8    val remove_thy: string -> unit
     2.9    val kill_thy: string -> unit
    2.10    val use_theories:
    2.11 @@ -126,12 +125,6 @@
    2.12  
    2.13  val get_imports = Resources.imports_of o get_theory;
    2.14  
    2.15 -(*Proof General legacy*)
    2.16 -fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
    2.17 -  (case get_deps name of
    2.18 -    NONE => []
    2.19 -  | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
    2.20 -
    2.21  
    2.22  
    2.23  (** thy operations **)