further support for nested tooltips;
authorwenzelm
Fri Oct 05 14:32:56 2012 +0200 (2012-10-05)
changeset 49712a1bd8fe5131b
parent 49711 e5aaae7eadc9
child 49721 519cf2ac6c0e
further support for nested tooltips;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/pretty_tooltip.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 13:57:48 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 14:32:56 2012 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.{Component, Container, Frame}
     1.8 +import java.awt.{Component, Container, Frame, Window}
     1.9  
    1.10  import scala.annotation.tailrec
    1.11  
    1.12 @@ -20,18 +20,31 @@
    1.13  
    1.14  object JEdit_Lib
    1.15  {
    1.16 -  /* frames */
    1.17 +  /* GUI components */
    1.18 +
    1.19 +  def get_parent(component: Component): Option[Container] =
    1.20 +    component.getParent match {
    1.21 +      case null => None
    1.22 +      case parent => Some(parent)
    1.23 +    }
    1.24 +
    1.25 +  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    1.26 +    private var next_elem = get_parent(component)
    1.27 +    def hasNext(): Boolean = next_elem.isDefined
    1.28 +    def next(): Container =
    1.29 +      next_elem match {
    1.30 +        case Some(parent) =>
    1.31 +          next_elem = get_parent(parent)
    1.32 +          parent
    1.33 +        case None => Iterator.empty.next()
    1.34 +      }
    1.35 +  }
    1.36 +
    1.37 +  def parent_window(component: Component): Option[Window] =
    1.38 +    ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
    1.39  
    1.40    def parent_frame(component: Component): Option[Frame] =
    1.41 -  {
    1.42 -    @tailrec def find(c: Container): Option[Frame] =
    1.43 -      c match {
    1.44 -        case null => None
    1.45 -        case frame: Frame => Some(frame)
    1.46 -        case _ => find(c.getParent)
    1.47 -      }
    1.48 -    find(component.getParent)
    1.49 -  }
    1.50 +    ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
    1.51  
    1.52  
    1.53    /* buffers */
     2.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 13:57:48 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 14:32:56 2012 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 -import java.awt.{Toolkit, Color, Point, BorderLayout}
     2.8 +import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
     2.9  import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
    2.10  import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
    2.11  import javax.swing.border.LineBorder
    2.12 @@ -23,19 +23,28 @@
    2.13    text_area: TextArea,
    2.14    rendering: Isabelle_Rendering,
    2.15    mouse_x: Int, mouse_y: Int, body: XML.Body)
    2.16 -  extends JWindow(JEdit_Lib.parent_frame(text_area) getOrElse view)
    2.17 +  extends JWindow(JEdit_Lib.parent_window(text_area) getOrElse view)
    2.18  {
    2.19    window =>
    2.20  
    2.21    window.addWindowFocusListener(new WindowAdapter {
    2.22 -    override def windowLostFocus(e: WindowEvent) { window.dispose() }
    2.23 +    override def windowLostFocus(e: WindowEvent) {
    2.24 +      if (!Window.getWindows.exists(w =>
    2.25 +            w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
    2.26 +        window.dispose()
    2.27 +    }
    2.28    })
    2.29  
    2.30    window.setContentPane(new JPanel(new BorderLayout) {
    2.31      private val action_listener = new ActionListener {
    2.32        def actionPerformed(e: ActionEvent) {
    2.33          e.getActionCommand match {
    2.34 -          case "close" => window.dispose()
    2.35 +          case "close" =>
    2.36 +            window.dispose()
    2.37 +            JEdit_Lib.ancestors(window) foreach {
    2.38 +              case c: Pretty_Tooltip => c.dispose
    2.39 +              case _ =>
    2.40 +            }
    2.41            case _ =>
    2.42          }
    2.43        }