adapted ThyLoad.deps_thy;
authorwenzelm
Sun Jul 29 22:42:00 2007 +0200 (2007-07-29)
changeset 2406769b51bc5ce06
parent 24066 fb455cb475df
child 24068 245b7e68a3bc
adapted ThyLoad.deps_thy;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 29 22:41:59 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 29 22:42:00 2007 +0200
     1.3 @@ -692,14 +692,14 @@
     1.4  
     1.5          fun filerefs f =
     1.6              let val thy = thy_name f
     1.7 -                val (_, (_,filerefs)) = ThyLoad.deps_thy (Path.dir f) thy true
     1.8 +                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy true)
     1.9              in
    1.10                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
    1.11                                       name=NONE, idtables=[], fileurls=filerefs})
    1.12              end
    1.13  
    1.14          fun thyrefs thy =
    1.15 -            let val (_, (thyrefs,_)) = ThyLoad.deps_thy Path.current thy true
    1.16 +            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy true)
    1.17              in
    1.18                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
    1.19                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,