# HG changeset patch
# User berghofe
# Date 1093278678 -7200
# Node ID daa9f645a26eddb01ffede172122137fae1f105d
# Parent  6cdd6a8da9b9de2c0a98927922ce9b4d5f4ece9a
Adapted to new interface of function ThyLoad.check_file

diff -r 6cdd6a8da9b9 -r daa9f645a26e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 23 17:06:18 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 23 18:31:18 2004 +0200
@@ -296,7 +296,7 @@
     val pos = Path.position path;
     val (name', parents, files) = ThyHeader.scan (src, pos);
     val ml_path = ThyLoad.ml_path name;
-    val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
+    val ml_file = if ml andalso is_some (ThyLoad.check_file None ml_path) then [ml_path] else [];
   in
     if name <> name' then
       error ("Filename " ^ quote (Path.pack path) ^
@@ -315,7 +315,7 @@
     val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
     val tr_name = if time then "time_use" else "use";
   in
-    if is_none (ThyLoad.check_file path) then ()
+    if is_none (ThyLoad.check_file None path) then ()
     else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   end;
 
diff -r 6cdd6a8da9b9 -r daa9f645a26e src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Aug 23 17:06:18 2004 +0200
+++ b/src/Pure/proof_general.ML	Mon Aug 23 18:31:18 2004 +0200
@@ -393,7 +393,7 @@
 fun try_update_thy_only file =
   ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
     let val name = thy_name file in
-      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) 
+      if is_some (ThyLoad.check_file None (ThyLoad.thy_path name)) 
       then update_thy_only name
       else warning ("Unkown theory context of ML file." ^ which_context ())
     end) ();