src/Tools/jEdit/src/pretty_text_area.scala

           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
             text_area.selectAll
             evt.consume
 
           case KeyEvent.VK_ESCAPE =>
-            if (PIDE.dismissed_popups(view)) evt.consume
+            if (Isabelle.dismissed_popups(view)) evt.consume
 
           case _ =>
         }
         if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
       },