prefer sequential file-system access, but parallel parse;
authorwenzelm
Wed Sep 27 11:29:50 2017 +0200 (21 months ago)
changeset 666985b9dc3f7bcde
parent 66697 190834aa43a7
child 66699 16fd7655d39d
prefer sequential file-system access, but parallel parse;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Sep 27 11:11:07 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 11:29:50 2017 +0200
     1.3 @@ -57,16 +57,18 @@
     1.4  
     1.5    /* theory files */
     1.6  
     1.7 -  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
     1.8 +  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
     1.9    {
    1.10      val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
    1.11 -    if (syntax.load_commands_in(text)) {
    1.12 -      val spans = syntax.parse_spans(text)
    1.13 -      val dir = Path.explode(name.master_dir)
    1.14 -      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    1.15 -        map(a => dir + Path.explode(a)).toList
    1.16 +    () => {
    1.17 +      if (syntax.load_commands_in(text)) {
    1.18 +        val spans = syntax.parse_spans(text)
    1.19 +        val dir = Path.explode(name.master_dir)
    1.20 +        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    1.21 +          map(a => dir + Path.explode(a)).toList
    1.22 +      }
    1.23 +      else Nil
    1.24      }
    1.25 -    else Nil
    1.26    }
    1.27  
    1.28    def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
    1.29 @@ -77,7 +79,7 @@
    1.30        val files =
    1.31          for {
    1.32            (path, (_, theory)) <- roots zip Thy_Header.ml_roots
    1.33 -          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))
    1.34 +          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
    1.35          } yield file
    1.36        roots ::: files
    1.37      }
     2.1 --- a/src/Pure/Thy/thy_info.scala	Wed Sep 27 11:11:07 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Sep 27 11:29:50 2017 +0200
     2.3 @@ -90,8 +90,8 @@
     2.4  
     2.5      def loaded_files: List[Path] =
     2.6      {
     2.7 -      val dep_files =
     2.8 -        Par_List.map((dep: Thy_Info.Dep) => resources.loaded_files(syntax, dep.name), rev_deps)
     2.9 +      val parses = rev_deps.map(dep => resources.loaded_files(syntax, dep.name))
    2.10 +      val dep_files = Par_List.map((parse: () => List[Path]) => parse(), parses)
    2.11        ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
    2.12      }
    2.13