equal
deleted
inserted
replaced
590 |
590 |
591 val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
591 val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
592 |
592 |
593 fun filerefs f = |
593 fun filerefs f = |
594 let val thy = thy_name f |
594 let val thy = thy_name f |
595 val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy)) |
|
596 in |
595 in |
597 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, |
596 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, |
598 name=NONE, idtables=[], fileurls=filerefs}) |
597 name=NONE, idtables=[], fileurls=[]}) |
599 end |
598 end |
600 |
599 |
601 fun thyrefs thy = |
600 fun thyrefs thy = |
602 let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy)) |
601 let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy)) |
603 in |
602 in |