clarified pure_files, based on uniform loaded_files;
authorwenzelm
Tue Sep 26 22:30:54 2017 +0200 (19 months ago)
changeset 666968f863dae78a0
parent 66695 91500c024c7f
child 66697 190834aa43a7
clarified pure_files, based on uniform loaded_files;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Sep 26 20:54:40 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Sep 26 22:30:54 2017 +0200
     1.3 @@ -57,20 +57,32 @@
     1.4  
     1.5    /* theory files */
     1.6  
     1.7 -  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
     1.8 -    if (syntax.load_commands_in(text)) {
     1.9 -      val spans = syntax.parse_spans(text)
    1.10 -      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
    1.11 -    }
    1.12 -    else Nil
    1.13 -
    1.14    def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
    1.15    {
    1.16      val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
    1.17 -    val dir = Path.explode(name.master_dir)
    1.18 -    loaded_files(syntax, text).map(a => dir + Path.explode(a))
    1.19 +    if (syntax.load_commands_in(text)) {
    1.20 +      val spans = syntax.parse_spans(text)
    1.21 +      val dir = Path.explode(name.master_dir)
    1.22 +      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    1.23 +        map(a => dir + Path.explode(a)).toList
    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 +    if (Sessions.is_pure(session)) {
    1.30 +      val roots =
    1.31 +        for { (name, theory) <- Thy_Header.ml_roots }
    1.32 +        yield ((dir + Path.explode(name)).expand, theory)
    1.33 +      val files =
    1.34 +        for {
    1.35 +          (path, theory) <- roots
    1.36 +          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))
    1.37 +        } yield file
    1.38 +      roots.map(_._1) ::: files
    1.39 +    }
    1.40 +    else Nil
    1.41 +
    1.42    def theory_qualifier(name: Document.Node.Name): String =
    1.43      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
    1.44  
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Sep 26 20:54:40 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Sep 26 22:30:54 2017 +0200
     2.3 @@ -200,16 +200,7 @@
     2.4              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
     2.5              val loaded_files =
     2.6                if (inlined_files) {
     2.7 -                val pure_files =
     2.8 -                  if (is_pure(info.name)) {
     2.9 -                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
    2.10 -                    val files =
    2.11 -                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
    2.12 -                        map(file => info.dir + Path.explode(file))
    2.13 -                    roots ::: files
    2.14 -                  }
    2.15 -                  else Nil
    2.16 -                pure_files ::: thy_deps.loaded_files
    2.17 +                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
    2.18                }
    2.19                else Nil
    2.20