--- a/src/Tools/jEdit/src/jedit_resources.scala Sun Apr 09 21:06:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 10 11:29:47 2017 +0200
@@ -28,7 +28,7 @@
def node_name(buffer: Buffer): Document.Node.Name =
{
val node = JEdit_Lib.buffer_name(buffer)
- val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+ val theory = Thy_Header.theory_name(node)
val master_dir = if (theory == "") "" else buffer.getDirectory
Document.Node.Name(node, master_dir, theory)
}
@@ -37,7 +37,7 @@
{
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
- val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+ val theory = Thy_Header.theory_name(node)
val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
Document.Node.Name(node, master_dir, theory)
}