# HG changeset patch
# User wenzelm
# Date 935001676 -7200
# Node ID 28d95a7a265abbce161e91da84b6f3a6a452aac2
# Parent  32a867ed94545a4c41fab58e672497a46f260b88
isa_action: don't lock pretend_used files;

diff -r 32a867ed9454 -r 28d95a7a265a src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Aug 18 20:40:28 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Aug 18 20:41:16 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Configuration for ProofGeneral of LFCS Edinburgh.
+Configuration for Proof General of LFCS Edinburgh.
 *)
 
 signature PROOF_GENERAL =
@@ -136,8 +136,14 @@
 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
 
 fun isa_action action name =
-  let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
-    if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
+  let
+    val update = (action = ThyInfo.Update);
+    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);
+  in
+    if update then seq (tell_pg "this file is loaded:") files
     else seq (tell_pg "you can unlock the file") files
   end;
 
@@ -156,7 +162,7 @@
 val show_context = Context.the_context;
 
 fun kill_goal () =
-  (Goals.reset_goals (); writeln ("Proof General, please clear the goals buffer."));
+  (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
 
 fun repeat_undo 0 = ()
   | repeat_undo n = (undo(); repeat_undo (n - 1));
@@ -165,7 +171,7 @@
  (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   ThyInfo.touch_all_thys ();
   kill_goal ();
-  writeln ("Proof General, please clear the response buffer.");
+  writeln "Proof General, please clear the response buffer.";
   writeln "Isabelle Proof General: Isabelle process ready!");