src/Pure/Interface/proof_general.ML
changeset 7266 28d95a7a265a
parent 7235 3c3defaad8ae
child 7289 3b1b301467cd
     1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Aug 18 20:40:28 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Aug 18 20:41:16 1999 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Configuration for ProofGeneral of LFCS Edinburgh.
     1.8 +Configuration for Proof General of LFCS Edinburgh.
     1.9  *)
    1.10  
    1.11  signature PROOF_GENERAL =
    1.12 @@ -136,8 +136,14 @@
    1.13  fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
    1.14  
    1.15  fun isa_action action name =
    1.16 -  let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
    1.17 -    if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
    1.18 +  let
    1.19 +    val update = (action = ThyInfo.Update);
    1.20 +    fun loaded ((path, _), really) =
    1.21 +      if update andalso not really then None
    1.22 +      else Some (File.sysify_path path);
    1.23 +    val files = mapfilter loaded (ThyInfo.loaded_files name);
    1.24 +  in
    1.25 +    if update then seq (tell_pg "this file is loaded:") files
    1.26      else seq (tell_pg "you can unlock the file") files
    1.27    end;
    1.28  
    1.29 @@ -156,7 +162,7 @@
    1.30  val show_context = Context.the_context;
    1.31  
    1.32  fun kill_goal () =
    1.33 -  (Goals.reset_goals (); writeln ("Proof General, please clear the goals buffer."));
    1.34 +  (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
    1.35  
    1.36  fun repeat_undo 0 = ()
    1.37    | repeat_undo n = (undo(); repeat_undo (n - 1));
    1.38 @@ -165,7 +171,7 @@
    1.39   (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
    1.40    ThyInfo.touch_all_thys ();
    1.41    kill_goal ();
    1.42 -  writeln ("Proof General, please clear the response buffer.");
    1.43 +  writeln "Proof General, please clear the response buffer.";
    1.44    writeln "Isabelle Proof General: Isabelle process ready!");
    1.45  
    1.46