src/Tools/jEdit/src/jedit_resources.scala
changeset 63022 785a59235a15
parent 61023 46df28442a80
child 64797 891a25a87ea1
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 18 22:51:32 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 19 12:06:34 2016 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    def node_name(buffer: Buffer): Document.Node.Name =
     1.5    {
     1.6      val node = JEdit_Lib.buffer_name(buffer)
     1.7 -    val theory = Thy_Header.thy_name(node).getOrElse("")
     1.8 +    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
     1.9      val master_dir = if (theory == "") "" else buffer.getDirectory
    1.10      Document.Node.Name(node, master_dir, theory)
    1.11    }