tuned;
authorwenzelm
Tue Sep 26 20:54:40 2017 +0200 (19 months ago)
changeset 6669591500c024c7f
parent 66694 41177b124067
child 66696 8f863dae78a0
tuned;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Sep 26 17:32:16 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Sep 26 20:54:40 2017 +0200
     1.3 @@ -64,6 +64,13 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 +  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
     1.8 +  {
     1.9 +    val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
    1.10 +    val dir = Path.explode(name.master_dir)
    1.11 +    loaded_files(syntax, text).map(a => dir + Path.explode(a))
    1.12 +  }
    1.13 +
    1.14    def theory_qualifier(name: Document.Node.Name): String =
    1.15      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
    1.16  
     2.1 --- a/src/Pure/Thy/thy_info.scala	Tue Sep 26 17:32:16 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Sep 26 20:54:40 2017 +0200
     2.3 @@ -90,14 +90,8 @@
     2.4  
     2.5      def loaded_files: List[Path] =
     2.6      {
     2.7 -      def loaded(dep: Thy_Info.Dep): List[Path] =
     2.8 -      {
     2.9 -        val string = resources.with_thy_reader(dep.name,
    2.10 -          reader => Symbol.decode(reader.source.toString))
    2.11 -        resources.loaded_files(syntax, string).
    2.12 -          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    2.13 -      }
    2.14 -      val dep_files = Par_List.map(loaded _, rev_deps)
    2.15 +      val dep_files =
    2.16 +        Par_List.map((dep: Thy_Info.Dep) => resources.loaded_files(syntax, dep.name), rev_deps)
    2.17        ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
    2.18      }
    2.19