--- a/src/Pure/Thy/thy_load.ML Sat Nov 16 18:34:11 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Nov 16 19:23:16 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Thy/thy_load.ML
Author: Makarius
-Loading files that contribute to a theory. Global master path for TTY loop.
+Loading files that contribute to a theory.
*)
signature THY_LOAD =
@@ -122,11 +122,6 @@
val id = SHA1.digest text;
in ((full_path, id), text) end;
-(*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;
-
fun loaded_files_current thy =
#provided (Files.get thy) |>
forall (fn (src_path, id) =>
@@ -134,6 +129,11 @@
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_thy *)