# HG changeset patch
# User wenzelm
# Date 1207832009 -7200
# Node ID 725a3d9011d120e81137f7236aa118f0e573a50b
# Parent  f9c3c2110b031717a366b8c569e9015e7256e8f3
ThyInfo.get_names;

diff -r f9c3c2110b03 -r 725a3d9011d1 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 10 14:53:28 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 10 14:53:29 2008 +0200
@@ -167,7 +167,7 @@
 
 in
   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
-  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
+  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
 end;
 
 
diff -r f9c3c2110b03 -r 725a3d9011d1 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 14:53:28 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 14:53:29 2008 +0200
@@ -340,7 +340,7 @@
 
 in
   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
-  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
+  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
 end;
 
 
@@ -656,13 +656,13 @@
     in 
         case (thyname,objtype) of
            (NONE, NONE) =>
-           setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
+           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
          | (NONE, SOME ObjFile) =>
-           setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
+           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
          | (SOME fi, SOME ObjFile) =>
            setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
          | (NONE, SOME ObjTheory) =>
-           setids (idtable ObjTheory NONE (ThyInfo.names()))
+           setids (idtable ObjTheory NONE (ThyInfo.get_names()))
          | (SOME thy, SOME ObjTheory) =>
            setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
          | (SOME thy, SOME ObjTheorem) =>
@@ -671,9 +671,9 @@
            (* A large query, but not unreasonable. ~5000 results for HOL.*)
            (* Several setids should be allowed, but Eclipse code is currently broken:
               List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
-                         (ThyInfo.names()) *)
+                         (ThyInfo.get_names()) *)
            setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
-                           (maps qualified_thms_of_thy (ThyInfo.names())))
+                           (maps qualified_thms_of_thy (ThyInfo.get_names())))
          | _ => warning ("askids: ignored argument combination")
     end