# HG changeset patch
# User wenzelm
# Date 1354884961 -3600
# Node ID 0d60de55c58a8e934da856440a2eb92dc6ce53e1
# Parent  e17a1f179bb02a28abb2962f592e5867a94c676c
fork slow part of Thy_Load.body_files only;

diff -r e17a1f179bb0 -r 0d60de55c58a src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:38:32 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:56:01 2012 +0100
@@ -84,16 +84,20 @@
         val future_header: JFuture[Exn.Result[Document.Node.Header]] =
           if (files) {
             val string = thy_load.with_thy_text(name, _.toString)
-            default_thread_pool.submit(() =>
-              Exn.capture {
-                try {
-                  val syntax0 = syntax.add_keywords(header0.keywords)
-                  val files = thy_load.theory_body_files(syntax0, string)
-                  header0.copy(uses = header0.uses ::: files.map((_, false)))
+            val syntax0 = syntax.add_keywords(header0.keywords)
+
+            if (thy_load.body_files_test(syntax0, string)) {
+              default_thread_pool.submit(() =>
+                Exn.capture {
+                  try {
+                    val files = thy_load.body_files(syntax0, string)
+                    header0.copy(uses = header0.uses ::: files.map((_, false)))
+                  }
+                  catch { case ERROR(msg) => err(msg) }
                 }
-                catch { case ERROR(msg) => err(msg) }
-              }
-            )
+              )
+            }
+            else Library.future_value(Exn.Res(header0))
           }
           else Library.future_value(Exn.Res(header0))
 
diff -r e17a1f179bb0 -r 0d60de55c58a src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:38:32 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:56:01 2012 +0100
@@ -80,27 +80,27 @@
     clean_tokens.reverse.find(_.is_name).map(_.content)
   }
 
-  def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
+  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
+    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+  def body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
     val thy_load_commands = syntax.thy_load_commands
-    if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
-      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-      spans.iterator.map({
-        case toks @ (tok :: _) if tok.is_command =>
-          thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
-            case Some((_, exts)) =>
-              find_file(toks) match {
-                case Some(file) =>
-                  if (exts.isEmpty) List(file)
-                  else exts.map(ext => file + "." + ext)
-                case None => Nil
-              }
-            case None => Nil
-          }
-        case _ => Nil
-      }).flatten.toList
-    }
-    else Nil
+    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+    spans.iterator.map({
+      case toks @ (tok :: _) if tok.is_command =>
+        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
+          case Some((_, exts)) =>
+            find_file(toks) match {
+              case Some(file) =>
+                if (exts.isEmpty) List(file)
+                else exts.map(ext => file + "." + ext)
+              case None => Nil
+            }
+          case None => Nil
+        }
+      case _ => Nil
+    }).flatten.toList
   }
 
   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =