explore theory_body_files via future, for improved performance;
further internalization of header errors;

--- a/src/Pure/System/build.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Pure/System/build.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -376,9 +376,10 @@
           val syntax = thy_deps.make_syntax
 
           val all_files =
-            (thy_deps.deps.map({ case (n, h) =>
-              val thy = Path.explode(n.node)
-              val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
+            (thy_deps.deps.map({ case dep =>
+              val thy = Path.explode(dep.name.node)
+              val uses = dep.join_header.uses.map(p =>
+                Path.explode(dep.name.dir) + Path.explode(p._1))
               thy :: uses
             }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
 
@@ -392,7 +393,7 @@
                 error(msg + "\nThe error(s) above occurred in session " +
                   quote(name) + Position.here(info.pos))
             }
-          val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
+          val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
 
           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
       }))

--- a/src/Pure/Thy/thy_info.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.util.concurrent.{Future => JFuture}
+
+
 class Thy_Info(thy_load: Thy_Load)
 {
   /* messages */
@@ -24,7 +27,13 @@
 
   /* dependencies */
 
-  type Dep = (Document.Node.Name, Document.Node.Header)
+  sealed case class Dep(
+    name: Document.Node.Name,
+    header0: Document.Node.Header,
+    future_header: JFuture[Exn.Result[Document.Node.Header]])
+  {
+    def join_header: Document.Node.Header = Exn.release(future_header.get)
+  }
 
   object Dependencies
   {
@@ -37,7 +46,7 @@
     val seen: Set[Document.Node.Name])
   {
     def :: (dep: Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
+      new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
 
     def + (name: Document.Node.Name): Dependencies =
       new Dependencies(rev_deps, keywords, seen = seen + name)
@@ -45,7 +54,7 @@
     def deps: List[Dep] = rev_deps.reverse
 
     def loaded_theories: Set[String] =
-      (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
+      (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
 
     def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
@@ -60,24 +69,41 @@
     if (required.seen(name)) required
     else if (thy_load.loaded_theories(name.theory)) required + name
     else {
+      def err(msg: String): Nothing =
+        cat_error(msg, "The error(s) above occurred while examining theory " +
+          quote(name.theory) + required_by(initiators))
+
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val syntax = required.make_syntax
-        val header =
-          try {
-            if (files) thy_load.check_thy_files(syntax, name)
-            else thy_load.check_thy(name)
+
+        val header0 =
+          try { thy_load.check_thy(name) }
+          catch { case ERROR(msg) => err(msg) }
+
+        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)))
+                }
+                catch { case ERROR(msg) => err(msg) }
+              }
+            )
           }
-          catch {
-            case ERROR(msg) =>
-              cat_error(msg, "The error(s) above occurred while examining theory " +
-                quote(name.theory) + required_by(initiators))
-          }
-        (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
+          else Library.future_value(Exn.Res(header0))
+
+        Dep(name, header0, future_header) ::
+          require_thys(files, name :: initiators, required + name, header0.imports)
       }
       catch {
         case e: Throwable =>
-          (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
+          val bad_header = Document.Node.bad_header(Exn.message(e))
+          Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
       }
     }
   }

--- a/src/Pure/Thy/thy_load.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -80,7 +80,7 @@
     clean_tokens.reverse.find(_.is_name).map(_.content)
   }
 
-  def find_files(syntax: Outer_Syntax, text: String): List[String] =
+  def theory_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) })) {
@@ -105,28 +105,22 @@
 
   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   {
-    val header = Thy_Header.read(text)
+    try {
+      val header = Thy_Header.read(text)
 
-    val name1 = header.name
-    if (name.theory != name1)
-      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
-        " for theory " + quote(name1))
+      val name1 = header.name
+      if (name.theory != name1)
+        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
+          " for theory " + quote(name1))
 
-    val imports = header.imports.map(import_name(name.dir, _))
-    val uses = header.uses
-    Document.Node.Header(imports, header.keywords, uses)
+      val imports = header.imports.map(import_name(name.dir, _))
+      val uses = header.uses
+      Document.Node.Header(imports, header.keywords, uses)
+    }
+    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
     with_thy_text(name, check_thy_text(name, _))
-
-  def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, text =>
-      {
-        val string = text.toString
-        val header = check_thy_text(name, string)
-        val more_uses = find_files(syntax.add_keywords(header.keywords), string)
-        header.copy(uses = header.uses ::: more_uses.map((_, false)))
-      })
 }
 

--- a/src/Pure/library.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Pure/library.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -10,6 +10,7 @@
 
 import java.lang.System
 import java.util.Locale
+import java.util.concurrent.{Future => JFuture, TimeUnit}
 import java.awt.Component
 import javax.swing.JOptionPane
 
@@ -187,6 +188,18 @@
     selection.index = 3
     prototypeDisplayValue = Some("00000%")
   }
+
+
+  /* Java futures */
+
+  def future_value[A](x: A) = new JFuture[A]
+  {
+    def cancel(may_interrupt: Boolean): Boolean = false
+    def isCancelled(): Boolean = false
+    def isDone(): Boolean = true
+    def get(): A = x
+    def get(timeout: Long, time_unit: TimeUnit): A = x
+  }
 }
 
 

--- a/src/Tools/jEdit/src/plugin.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -157,7 +157,7 @@
 
         val thy_info = new Thy_Info(PIDE.thy_load)
         // FIXME avoid I/O in Swing thread!?!
-        val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
+        val files = thy_info.dependencies(true, thys).deps.map(_.name.node).
           filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
         if (!files.isEmpty) {