--- 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) {
--- 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
}
)
--- 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
+ }
}
--- 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)
}
--- 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 _ =>
}