src/Tools/jEdit/src/graphview_dockable.scala
author wenzelm
Sat Mar 23 19:39:31 2013 +0100 (2013-03-23 ago)
changeset 51496 cb677987b7e3
parent 51449 8d6e478934dc
child 52480 6a762cda56bd
permissions -rw-r--r--
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm@49570
     1
/*  Title:      Tools/jEdit/src/graphview_dockable.scala
wenzelm@49566
     2
    Author:     Makarius
markus@49557
     3
wenzelm@50452
     4
Stateless dockable window for graphview.
markus@49557
     5
*/
markus@49557
     6
wenzelm@49566
     7
package isabelle.jedit
markus@49557
     8
markus@49557
     9
markus@49557
    10
import isabelle._
wenzelm@49566
    11
wenzelm@50452
    12
import javax.swing.JComponent
wenzelm@50452
    13
import java.awt.event.{WindowFocusListener, WindowEvent}
markus@49557
    14
markus@49557
    15
import org.gjt.sp.jedit.View
markus@49557
    16
wenzelm@50452
    17
import scala.swing.TextArea
wenzelm@50452
    18
wenzelm@50452
    19
wenzelm@50452
    20
object Graphview_Dockable
wenzelm@50452
    21
{
wenzelm@50452
    22
  /* implicit arguments -- owned by Swing thread */
wenzelm@50452
    23
wenzelm@50452
    24
  private var implicit_snapshot = Document.State.init.snapshot()
wenzelm@50452
    25
wenzelm@50452
    26
  private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
wenzelm@50452
    27
  private var implicit_graph = no_graph
wenzelm@50452
    28
wenzelm@50452
    29
  private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
wenzelm@50452
    30
  {
wenzelm@50452
    31
    Swing_Thread.require()
wenzelm@50452
    32
wenzelm@50452
    33
    implicit_snapshot = snapshot
wenzelm@50452
    34
    implicit_graph = graph
wenzelm@50452
    35
  }
wenzelm@50452
    36
wenzelm@50452
    37
  private def reset_implicit(): Unit =
wenzelm@50452
    38
    set_implicit(Document.State.init.snapshot(), no_graph)
wenzelm@50452
    39
wenzelm@50452
    40
  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
wenzelm@50452
    41
  {
wenzelm@50452
    42
    set_implicit(snapshot, graph)
wenzelm@50452
    43
    view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
wenzelm@50452
    44
  }
wenzelm@50452
    45
}
wenzelm@50452
    46
markus@49557
    47
wenzelm@49570
    48
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
markus@49557
    49
{
wenzelm@49566
    50
  Swing_Thread.require()
wenzelm@49566
    51
wenzelm@50452
    52
  private val snapshot = Graphview_Dockable.implicit_snapshot
wenzelm@50452
    53
  private val graph = Graphview_Dockable.implicit_graph
wenzelm@50446
    54
wenzelm@50452
    55
  private val window_focus_listener =
wenzelm@50452
    56
    new WindowFocusListener {
wenzelm@50452
    57
      def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) }
wenzelm@50452
    58
      def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
wenzelm@50452
    59
    }
wenzelm@49566
    60
wenzelm@50452
    61
  val graphview =
wenzelm@50452
    62
    graph match {
wenzelm@50452
    63
      case Exn.Res(proper_graph) =>
wenzelm@50452
    64
        new isabelle.graphview.Main_Panel(proper_graph) {
wenzelm@50452
    65
          override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
wenzelm@50452
    66
          {
wenzelm@50452
    67
            val rendering = Rendering(snapshot, PIDE.options.value)
wenzelm@51496
    68
            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
wenzelm@51496
    69
              Text.Range(-1), body)
wenzelm@50452
    70
            null
wenzelm@49566
    71
          }
wenzelm@49566
    72
        }
wenzelm@50452
    73
      case Exn.Exn(exn) => new TextArea(Exn.message(exn))
markus@49557
    74
    }
wenzelm@50452
    75
  set_content(graphview)
markus@49557
    76
wenzelm@49566
    77
  override def init()
wenzelm@49566
    78
  {
wenzelm@49566
    79
    Swing_Thread.require()
wenzelm@50452
    80
    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
wenzelm@49566
    81
  }
wenzelm@49566
    82
wenzelm@49566
    83
  override def exit()
wenzelm@49566
    84
  {
wenzelm@49566
    85
    Swing_Thread.require()
wenzelm@50452
    86
    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
wenzelm@49566
    87
  }
markus@49557
    88
}