# HG changeset patch
# User wenzelm
# Date 1396549032 -7200
# Node ID bc118a32a870c1e011fa1fb8cf3afb4045b25040
# Parent  b33df983785074e262ba8e5767dc68d8a36e8a72
tuned signature (see also 0850d43cb355);

diff -r b33df9837850 -r bc118a32a870 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Apr 03 19:49:53 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 03 20:17:12 2014 +0200
@@ -50,13 +50,13 @@
 
   /* theory files */
 
-  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
-    syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
-
-  def body_files(syntax: Outer_Syntax, text: String): List[String] =
+  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
   {
-    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+    if (syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
+      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+      spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+    }
+    else Nil
   }
 
   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
diff -r b33df9837850 -r bc118a32a870 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Apr 03 19:49:53 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Apr 03 20:17:12 2014 +0200
@@ -31,12 +31,10 @@
     name: Document.Node.Name,
     header: Document.Node.Header)
   {
-    def load_files(syntax: Outer_Syntax): List[String] =
+    def loaded_files(syntax: Outer_Syntax): List[String] =
     {
       val string = resources.with_thy_text(name, _.toString)
-      if (resources.body_files_test(syntax, string))
-        resources.body_files(syntax, string)
-      else Nil
+      resources.loaded_files(syntax, string)
     }
   }
 
@@ -87,12 +85,12 @@
     def loaded_theories: Set[String] =
       (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
 
-    def load_files: List[Path] =
+    def loaded_files: List[Path] =
     {
       val dep_files =
         rev_deps.par.map(dep =>
           Exn.capture {
-            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
+            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
           }).toList
       ((Nil: List[Path]) /: dep_files) {
         case (acc_files, files) => Exn.release(files) ::: acc_files
diff -r b33df9837850 -r bc118a32a870 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 03 19:49:53 2014 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 03 20:17:12 2014 +0200
@@ -443,10 +443,10 @@
             val keywords = thy_deps.keywords
             val syntax = thy_deps.syntax
 
-            val body_files = if (inlined_files) thy_deps.load_files else Nil
+            val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
 
             val all_files =
-              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
                 info.files.map(file => info.dir + file)).map(_.expand)
 
             if (list_files) {