690 |
690 |
691 val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
691 val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
692 |
692 |
693 fun filerefs f = |
693 fun filerefs f = |
694 let val thy = thy_name f |
694 let val thy = thy_name f |
695 val (_,filerefs) = OuterSyntax.deps_thy thy true f (* (Path.unpack f); *) |
695 val (_, (_,filerefs)) = ThyLoad.deps_thy [Path.dir f] thy true |
696 in |
696 in |
697 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, |
697 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, |
698 name=NONE, idtables=[], fileurls=filerefs}) |
698 name=NONE, idtables=[], fileurls=filerefs}) |
699 end |
699 end |
700 |
700 |
701 fun thyrefs thy = |
701 fun thyrefs thy = |
702 let val ml_path = ThyLoad.ml_path thy |
702 let val (_, (thyrefs,_)) = ThyLoad.deps_thy [] thy true |
703 val (thyrefs,_) = OuterSyntax.deps_thy thy true ml_path (* (Path.unpack f); *) |
|
704 in |
703 in |
705 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, |
704 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, |
706 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, |
705 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, |
707 ids=thyrefs}], fileurls=[]}) |
706 ids=thyrefs}], fileurls=[]}) |
708 end |
707 end |