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