# HG changeset patch
# User wenzelm
# Date 1489522264 -3600
# Node ID fe5a96240749f23e7a07e3b0f93e78b084287255
# Parent  509a9b0ad02e42ceb2027e719ce668e0630f3ada
clarified modules;

diff -r 509a9b0ad02e -r fe5a96240749 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Tue Mar 14 20:50:21 2017 +0100
+++ b/src/Tools/jEdit/src/context_menu.scala	Tue Mar 14 21:11:04 2017 +0100
@@ -23,7 +23,7 @@
   def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
     if (evt == null) null
     else {
-      PIDE.dismissed_popups(text_area.getView)
+      Isabelle.dismissed_popups(text_area.getView)
 
       val items1 =
         if (evt != null && evt.getSource == text_area.getPainter) {
diff -r 509a9b0ad02e -r fe5a96240749 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Mar 14 20:50:21 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Mar 14 21:11:04 2017 +0100
@@ -174,7 +174,7 @@
     JEdit_Lib.key_listener(
       key_pressed = (evt: KeyEvent) =>
         {
-          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
+          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Isabelle.dismissed_popups(text_area.getView))
             evt.consume
         }
     )
diff -r 509a9b0ad02e -r fe5a96240749 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 20:50:21 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 21:11:04 2017 +0100
@@ -461,4 +461,19 @@
     jEdit.setProperty("Plugin Options.last", "isabelle-general")
     new CombinedOptions(frame, 1)
   }
+
+
+  /* popups */
+
+  def dismissed_popups(view: View): Boolean =
+  {
+    var dismissed = false
+
+    JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
+      if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
+
+    if (Pretty_Tooltip.dismissed_all()) dismissed = true
+
+    dismissed
+  }
 }
diff -r 509a9b0ad02e -r fe5a96240749 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 20:50:21 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:11:04 2017 +0100
@@ -55,21 +55,6 @@
   lazy val editor = new JEdit_Editor
 
 
-  /* popups */
-
-  def dismissed_popups(view: View): Boolean =
-  {
-    var dismissed = false
-
-    JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
-      if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
-
-    if (Pretty_Tooltip.dismissed_all()) dismissed = true
-
-    dismissed
-  }
-
-
   /* document model and view */
 
   def exit_models(buffers: List[Buffer])
@@ -368,7 +353,7 @@
                 PIDE.init_view(buffer, text_area)
             }
             else {
-              PIDE.dismissed_popups(text_area.getView)
+              Isabelle.dismissed_popups(text_area.getView)
               PIDE.exit_view(buffer, text_area)
             }
 
diff -r 509a9b0ad02e -r fe5a96240749 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Mar 14 20:50:21 2017 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Mar 14 21:11:04 2017 +0100
@@ -251,7 +251,7 @@
             evt.consume
 
           case KeyEvent.VK_ESCAPE =>
-            if (PIDE.dismissed_popups(view)) evt.consume
+            if (Isabelle.dismissed_popups(view)) evt.consume
 
           case _ =>
         }