src/Tools/jEdit/src/graphview_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 65131 5d35f4bccfa7
permissions -rw-r--r--
tuned signature;
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@53247
    12
import javax.swing.JComponent
wenzelm@59286
    13
import java.awt.{Point, Font}
wenzelm@50452
    14
import java.awt.event.{WindowFocusListener, WindowEvent}
markus@49557
    15
markus@49557
    16
import org.gjt.sp.jedit.View
markus@49557
    17
wenzelm@50452
    18
import scala.swing.TextArea
wenzelm@50452
    19
wenzelm@50452
    20
wenzelm@50452
    21
object Graphview_Dockable
wenzelm@50452
    22
{
wenzelm@57612
    23
  /* implicit arguments -- owned by GUI thread */
wenzelm@50452
    24
wenzelm@52972
    25
  private var implicit_snapshot = Document.Snapshot.init
wenzelm@50452
    26
wenzelm@59245
    27
  private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph"))
wenzelm@50452
    28
  private var implicit_graph = no_graph
wenzelm@50452
    29
wenzelm@59245
    30
  private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
wenzelm@50452
    31
  {
wenzelm@57612
    32
    GUI_Thread.require {}
wenzelm@50452
    33
wenzelm@50452
    34
    implicit_snapshot = snapshot
wenzelm@50452
    35
    implicit_graph = graph
wenzelm@50452
    36
  }
wenzelm@50452
    37
wenzelm@50452
    38
  private def reset_implicit(): Unit =
wenzelm@52972
    39
    set_implicit(Document.Snapshot.init, no_graph)
wenzelm@50452
    40
wenzelm@59245
    41
  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
wenzelm@50452
    42
  {
wenzelm@50452
    43
    set_implicit(snapshot, graph)
wenzelm@50452
    44
    view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
wenzelm@50452
    45
  }
wenzelm@50452
    46
}
wenzelm@50452
    47
markus@49557
    48
wenzelm@49570
    49
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
markus@49557
    50
{
wenzelm@50452
    51
  private val snapshot = Graphview_Dockable.implicit_snapshot
wenzelm@59228
    52
  private val graph_result = Graphview_Dockable.implicit_graph
wenzelm@50446
    53
wenzelm@50452
    54
  private val window_focus_listener =
wenzelm@50452
    55
    new WindowFocusListener {
wenzelm@59228
    56
      def windowGainedFocus(e: WindowEvent) {
wenzelm@59228
    57
        Graphview_Dockable.set_implicit(snapshot, graph_result) }
wenzelm@50452
    58
      def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
wenzelm@50452
    59
    }
wenzelm@49566
    60
wenzelm@50452
    61
  val graphview =
wenzelm@59228
    62
    graph_result match {
wenzelm@59228
    63
      case Exn.Res(graph) =>
wenzelm@59462
    64
        val graphview = new isabelle.graphview.Graphview(graph) {
wenzelm@59395
    65
          def options: Options = PIDE.options.value
wenzelm@59395
    66
wenzelm@50452
    67
          override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
wenzelm@50452
    68
          {
wenzelm@52494
    69
            Pretty_Tooltip.invoke(() =>
wenzelm@52494
    70
              {
wenzelm@64621
    71
                val rendering = JEdit_Rendering(snapshot, options)
wenzelm@52496
    72
                val info = Text.Info(Text.Range(~1), body)
wenzelm@53247
    73
                Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
wenzelm@52494
    74
              })
wenzelm@50452
    75
            null
wenzelm@49566
    76
          }
wenzelm@59395
    77
wenzelm@59395
    78
          override def make_font(): Font =
wenzelm@61176
    79
            if (editor_style) Font_Info.main(PIDE.options.real("graphview_font_scale")).font
wenzelm@61176
    80
            else
wenzelm@61176
    81
              GUI.imitate_font(Font_Info.main().font,
wenzelm@61176
    82
                options.string("graphview_font_family"),
wenzelm@61176
    83
                options.real("graphview_font_scale"))
wenzelm@61176
    84
wenzelm@61176
    85
          override def foreground_color =
wenzelm@61176
    86
            if (editor_style) view.getTextArea.getPainter.getForeground
wenzelm@61176
    87
            else super.foreground_color
wenzelm@59395
    88
wenzelm@61176
    89
          override def background_color =
wenzelm@61176
    90
            if (editor_style) view.getTextArea.getPainter.getBackground
wenzelm@61176
    91
            else super.background_color
wenzelm@61176
    92
wenzelm@61176
    93
          override def selection_color =
wenzelm@61176
    94
            if (editor_style) view.getTextArea.getPainter.getSelectionColor
wenzelm@61176
    95
            else super.selection_color
wenzelm@61176
    96
wenzelm@61176
    97
          override def highlight_color =
wenzelm@61176
    98
            if (editor_style) view.getTextArea.getPainter.getLineHighlightColor
wenzelm@61176
    99
            else super.highlight_color
wenzelm@61176
   100
wenzelm@59233
   101
          override def error_color = PIDE.options.color_value("error_color")
wenzelm@61176
   102
wenzelm@61176
   103
          editor_style = true
wenzelm@49566
   104
        }
wenzelm@59459
   105
        new isabelle.graphview.Main_Panel(graphview)
wenzelm@50452
   106
      case Exn.Exn(exn) => new TextArea(Exn.message(exn))
markus@49557
   107
    }
wenzelm@50452
   108
  set_content(graphview)
markus@49557
   109
wenzelm@59288
   110
wenzelm@59396
   111
  override def focusOnDefaultComponent
wenzelm@59396
   112
  {
wenzelm@59396
   113
    graphview match {
wenzelm@59396
   114
      case main_panel: isabelle.graphview.Main_Panel =>
wenzelm@59396
   115
        main_panel.tree_panel.tree.requestFocusInWindow
wenzelm@59396
   116
      case _ =>
wenzelm@59396
   117
    }
wenzelm@59396
   118
  }
wenzelm@59396
   119
wenzelm@59396
   120
wenzelm@59288
   121
  /* main */
wenzelm@59288
   122
wenzelm@59288
   123
  private val main =
wenzelm@59288
   124
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@59288
   125
      case _: Session.Global_Options =>
wenzelm@59288
   126
        GUI_Thread.later {
wenzelm@59288
   127
          graphview match {
wenzelm@59288
   128
            case main_panel: isabelle.graphview.Main_Panel =>
wenzelm@59392
   129
              main_panel.update_layout()
wenzelm@59288
   130
            case _ =>
wenzelm@59288
   131
          }
wenzelm@59288
   132
        }
wenzelm@59288
   133
    }
wenzelm@59288
   134
wenzelm@49566
   135
  override def init()
wenzelm@49566
   136
  {
wenzelm@60215
   137
    GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
wenzelm@59288
   138
    PIDE.session.global_options += main
wenzelm@49566
   139
  }
wenzelm@49566
   140
wenzelm@49566
   141
  override def exit()
wenzelm@49566
   142
  {
wenzelm@60215
   143
    GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
wenzelm@59288
   144
    PIDE.session.global_options -= main
wenzelm@49566
   145
  }
markus@49557
   146
}