# HG changeset patch
# User wenzelm
# Date 1330634149 -3600
# Node ID e33519ec9e91f00982d3bde756bd73322db9aeb7
# Parent  40e2ada74ce8d943895cdcef32efb9731f8f9ca4# Parent  69efe9b2994ca0745cf56a07374765edb9ad0e2d
merged

diff -r 40e2ada74ce8 -r e33519ec9e91 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Thu Mar 01 19:35:02 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Thu Mar 01 21:35:49 2012 +0100
@@ -53,9 +53,8 @@
     }
   }
 
-  def check_thy(name: Document.Node.Name): Document.Node.Deps =
+  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps =
   {
-    val header = read_header(name)
     val name1 = header.name
     val imports = header.imports.map(import_name(name.dir, _))
     val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
@@ -63,5 +62,8 @@
       error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
     Document.Node.Deps(imports, uses)
   }
+
+  def check_thy(name: Document.Node.Name): Document.Node.Deps =
+    check_header(name, read_header(name))
 }
 
diff -r 40e2ada74ce8 -r e33519ec9e91 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 19:35:02 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 21:35:49 2012 +0100
@@ -258,7 +258,7 @@
           val node = nodes(name)
           val update_header =
             (node.header, header) match {
-              case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
               case _ => true
             }
           if (update_header) {
diff -r 40e2ada74ce8 -r e33519ec9e91 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 19:35:02 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 21:35:49 2012 +0100
@@ -61,12 +61,12 @@
   /* header */
 
   def node_header(): Document.Node_Header =
-  {
-    Swing_Thread.require()
-    if (Isabelle.jedit_buffer(name.node) == Some(buffer))
-      Exn.capture { Isabelle.thy_load.check_thy(name) }
-    else Exn.Exn(ERROR("Bad theory header"))  // FIXME odd race condition!?
-  }
+    Isabelle.swing_buffer_lock(buffer) {
+      Exn.capture {
+        Isabelle.thy_load.check_header(name,
+          Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+      }
+    }
 
 
   /* perspective */