Fixed problem with list_loaded_files and update().

Now when doing use_thy, we don't do an update.
Hopefully "following children are out of date"
message will be superfluous because they will be
unlocked already.  Will be re-read as needed.
Added update function.
Fixed up implementation of list_parents.

2 files changed, 3 insertions, 1 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 96bbf66e..9cec27a0 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -105,7 +105,8 @@ structure ProofGeneral =
           end
    in
     (writeln "Updating loaded files list...";
-     seq loading_msg thys_list)
+     seq loading_msg thys_list;
+     writeln "Done.")
    end;
 
  (* 
diff --git a/isa/isa.el b/isa/isa.el
index 534124ee..d39a1e0d 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -350,6 +350,7 @@ Resulting output from Isabelle will be parsed by Proof General."
 	   (file-name-sans-extension file))))
 
 
+
 ;; Next bits taken from isa-load.el
 ;; isa-load.el,v 3.8 1998/09/01