--- a/src/Tools/jEdit/src/document_model.scala Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Mar 15 20:35:47 2015 +0100
@@ -79,7 +79,8 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
+ PIDE.resources.check_thy_reader("", node_name,
+ JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))