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