--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Sep 01 15:15:29 2017 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Sep 01 15:21:10 2017 +0200
@@ -136,7 +136,7 @@
case Some((old, _ :: rest)) =>
rest match {
case top :: _ => top.request_focus
- case Nil => isabelle.jedit_base.JEdit_Lib.request_focus_view()
+ case Nil => JEdit_Lib.request_focus_view()
}
old.foreach(_.hide_popup)
tip.hide_popup
@@ -153,7 +153,7 @@
deactivate()
if (stack.isEmpty) false
else {
- isabelle.jedit_base.JEdit_Lib.request_focus_view()
+ JEdit_Lib.request_focus_view()
stack.foreach(_.hide_popup)
stack = Nil
true