ThyInfo.get_names;
authorwenzelm
Thu Apr 10 14:53:29 2008 +0200 (2008-04-10)
changeset 26613725a3d9011d1
parent 26612 f9c3c2110b03
child 26614 1f09a22a1027
ThyInfo.get_names;
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 10 14:53:28 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 10 14:53:29 2008 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5  in
     1.6    fun setup_thy_loader () = ThyInfo.add_hook trace_action;
     1.7 -  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
     1.8 +  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
     1.9  end;
    1.10  
    1.11  
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 14:53:28 2008 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 14:53:29 2008 +0200
     2.3 @@ -340,7 +340,7 @@
     2.4  
     2.5  in
     2.6    fun setup_thy_loader () = ThyInfo.add_hook trace_action;
     2.7 -  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
     2.8 +  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
     2.9  end;
    2.10  
    2.11  
    2.12 @@ -656,13 +656,13 @@
    2.13      in 
    2.14          case (thyname,objtype) of
    2.15             (NONE, NONE) =>
    2.16 -           setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
    2.17 +           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
    2.18           | (NONE, SOME ObjFile) =>
    2.19 -           setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
    2.20 +           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
    2.21           | (SOME fi, SOME ObjFile) =>
    2.22             setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
    2.23           | (NONE, SOME ObjTheory) =>
    2.24 -           setids (idtable ObjTheory NONE (ThyInfo.names()))
    2.25 +           setids (idtable ObjTheory NONE (ThyInfo.get_names()))
    2.26           | (SOME thy, SOME ObjTheory) =>
    2.27             setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
    2.28           | (SOME thy, SOME ObjTheorem) =>
    2.29 @@ -671,9 +671,9 @@
    2.30             (* A large query, but not unreasonable. ~5000 results for HOL.*)
    2.31             (* Several setids should be allowed, but Eclipse code is currently broken:
    2.32                List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
    2.33 -                         (ThyInfo.names()) *)
    2.34 +                         (ThyInfo.get_names()) *)
    2.35             setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
    2.36 -                           (maps qualified_thms_of_thy (ThyInfo.names())))
    2.37 +                           (maps qualified_thms_of_thy (ThyInfo.get_names())))
    2.38           | _ => warning ("askids: ignored argument combination")
    2.39      end
    2.40