src/Tools/jEdit/src/graphview_dockable.scala

more careful handling of Dialog_Result, with active area and color feedback;
more formal type Command.Results;
propagate command results to output, which is required to resolve update of dialog state;
clarified Markup.message: retain uninterpreted messages;

/*  Title:      Tools/jEdit/src/graphview_dockable.scala
    Author:     Makarius

Stateless dockable window for graphview.
*/

package isabelle.jedit


import isabelle._

import javax.swing.JComponent
import java.awt.event.{WindowFocusListener, WindowEvent}

import org.gjt.sp.jedit.View

import scala.swing.TextArea


object Graphview_Dockable
{
  /* implicit arguments -- owned by Swing thread */

  private var implicit_snapshot = Document.State.init.snapshot()

  private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
  private var implicit_graph = no_graph

  private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
  {
    Swing_Thread.require()

    implicit_snapshot = snapshot
    implicit_graph = graph
  }

  private def reset_implicit(): Unit =
    set_implicit(Document.State.init.snapshot(), no_graph)

  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
  {
    set_implicit(snapshot, graph)
    view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
  }
}


class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
{
  Swing_Thread.require()

  private val snapshot = Graphview_Dockable.implicit_snapshot
  private val graph = Graphview_Dockable.implicit_graph

  private val window_focus_listener =
    new WindowFocusListener {
      def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) }
      def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
    }

  val graphview =
    graph match {
      case Exn.Res(proper_graph) =>
        new isabelle.graphview.Main_Panel(proper_graph) {
          override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
          {
            val rendering = Rendering(snapshot, PIDE.options.value)
            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
            null
          }
        }
      case Exn.Exn(exn) => new TextArea(Exn.message(exn))
    }
  set_content(graphview)

  override def init()
  {
    Swing_Thread.require()
    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
  }

  override def exit()
  {
    Swing_Thread.require()
    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
  }
}