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)) = ThyLoad.deps_thy [Path.dir f] thy true |
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 (_, (thyrefs,_)) = ThyLoad.deps_thy [] thy true |
702 let val (_, (thyrefs,_)) = ThyLoad.deps_thy Path.current thy true |
703 in |
703 in |
704 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, |
704 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, |
705 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, |
705 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, |
706 ids=thyrefs}], fileurls=[]}) |
706 ids=thyrefs}], fileurls=[]}) |
707 end |
707 end |