# HG changeset patch
# User wenzelm
# Date 1483894424 -3600
# Node ID d67253005c0c9569c245c6cedacb022f24d6aeb8
# Parent  842163abfc0dfe4b3df794f26286cb00f102d73c
tuned;

diff -r 842163abfc0d -r d67253005c0c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 17:42:31 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 17:53:44 2017 +0100
@@ -38,10 +38,10 @@
   def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
 
   def visible_node(name: Document.Node.Name): Boolean =
-    JEdit_Lib.jedit_buffer(name) match {
-      case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
-      case None => false
-    }
+    (for {
+      text_area <- JEdit_Lib.jedit_text_areas()
+      doc_view <- Document_View(text_area)
+    } yield doc_view.model.node_name).contains(name)
 
 
   /* current situation */