tuned signature (see also 0850d43cb355);
authorwenzelm
Thu Apr 03 20:17:12 2014 +0200 (2014-04-03)
changeset 56392bc118a32a870
parent 56391 b33df9837850
child 56393 22f533e6a049
tuned signature (see also 0850d43cb355);
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Apr 03 19:49:53 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Apr 03 20:17:12 2014 +0200
     1.3 @@ -50,13 +50,13 @@
     1.4  
     1.5    /* theory files */
     1.6  
     1.7 -  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
     1.8 -    syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
     1.9 -
    1.10 -  def body_files(syntax: Outer_Syntax, text: String): List[String] =
    1.11 +  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
    1.12    {
    1.13 -    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    1.14 -    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    1.15 +    if (syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    1.16 +      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    1.17 +      spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    1.18 +    }
    1.19 +    else Nil
    1.20    }
    1.21  
    1.22    def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
     2.1 --- a/src/Pure/Thy/thy_info.scala	Thu Apr 03 19:49:53 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Apr 03 20:17:12 2014 +0200
     2.3 @@ -31,12 +31,10 @@
     2.4      name: Document.Node.Name,
     2.5      header: Document.Node.Header)
     2.6    {
     2.7 -    def load_files(syntax: Outer_Syntax): List[String] =
     2.8 +    def loaded_files(syntax: Outer_Syntax): List[String] =
     2.9      {
    2.10        val string = resources.with_thy_text(name, _.toString)
    2.11 -      if (resources.body_files_test(syntax, string))
    2.12 -        resources.body_files(syntax, string)
    2.13 -      else Nil
    2.14 +      resources.loaded_files(syntax, string)
    2.15      }
    2.16    }
    2.17  
    2.18 @@ -87,12 +85,12 @@
    2.19      def loaded_theories: Set[String] =
    2.20        (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    2.21  
    2.22 -    def load_files: List[Path] =
    2.23 +    def loaded_files: List[Path] =
    2.24      {
    2.25        val dep_files =
    2.26          rev_deps.par.map(dep =>
    2.27            Exn.capture {
    2.28 -            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    2.29 +            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    2.30            }).toList
    2.31        ((Nil: List[Path]) /: dep_files) {
    2.32          case (acc_files, files) => Exn.release(files) ::: acc_files
     3.1 --- a/src/Pure/Tools/build.scala	Thu Apr 03 19:49:53 2014 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 03 20:17:12 2014 +0200
     3.3 @@ -443,10 +443,10 @@
     3.4              val keywords = thy_deps.keywords
     3.5              val syntax = thy_deps.syntax
     3.6  
     3.7 -            val body_files = if (inlined_files) thy_deps.load_files else Nil
     3.8 +            val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
     3.9  
    3.10              val all_files =
    3.11 -              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
    3.12 +              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
    3.13                  info.files.map(file => info.dir + file)).map(_.expand)
    3.14  
    3.15              if (list_files) {