equal
deleted
inserted
replaced
88 (name.theory_base_name -> name.theory) // legacy |
88 (name.theory_base_name -> name.theory) // legacy |
89 } |
89 } |
90 |
90 |
91 def loaded_files: List[Path] = |
91 def loaded_files: List[Path] = |
92 { |
92 { |
93 def loaded(dep: Thy_Info.Dep): List[Path] = |
93 val dep_files = |
94 { |
94 Par_List.map((dep: Thy_Info.Dep) => resources.loaded_files(syntax, dep.name), rev_deps) |
95 val string = resources.with_thy_reader(dep.name, |
|
96 reader => Symbol.decode(reader.source.toString)) |
|
97 resources.loaded_files(syntax, string). |
|
98 map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) |
|
99 } |
|
100 val dep_files = Par_List.map(loaded _, rev_deps) |
|
101 ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } |
95 ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } |
102 } |
96 } |
103 |
97 |
104 override def toString: String = deps.toString |
98 override def toString: String = deps.toString |
105 } |
99 } |