# HG changeset patch
# User wenzelm
# Date 940525225 -7200
# Node ID b8dee46d778abd6b0964d64019c10394e5faffaf
# Parent  e54db490c537fd2ddab583005e49077910e6f0e3
tuned trace_action;

diff -r e54db490c537 -r b8dee46d778a src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Thu Oct 21 19:00:01 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Thu Oct 21 19:00:25 1999 +0200
@@ -146,13 +146,18 @@
 fun trace_action action name =
   let
     val update = (action = ThyInfo.Update);
-    fun loaded ((path, _), really) =
+    fun loaded (path, really) =
       if update andalso not really then None
-      else Some (File.sysify_path path);
-    val files = mapfilter loaded (ThyInfo.loaded_files name);
+      else Some path;
+    val tell = tell_pg (if update then "this file is loaded:" else "you can unlock the file")
+      o File.sysify_path;
+
+    val (master, files) = ThyInfo.loaded_files name;
   in
-    if update then seq (tell_pg "this file is loaded:") files
-    else seq (tell_pg "you can unlock the file") files
+    (case master of
+      Some path => tell path
+    | None => tell (ThyLoad.thy_path name));     (*just to make sure ...*)
+    seq tell (mapfilter loaded files)
   end;
 
 in