--- 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))
}
--- 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) {
--- 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 */