src/Tools/jEdit/src/jedit_resources.scala
changeset 65524 0910f1733909
parent 65501 b42743f5b595
child 65532 febfd9f78bd4
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 14:59:57 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 15:00:32 2017 +0200
@@ -26,7 +26,7 @@
   /* document node name */
 
   def known_file(path: String): Option[Document.Node.Name] =
-    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
 
   def node_name(path: String): Document.Node.Name =
     known_file(path) getOrElse {