stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;

--- a/src/Pure/General/graph.scala	Mon Dec 10 15:13:13 2012 +0100
+++ b/src/Pure/General/graph.scala	Mon Dec 10 15:17:47 2012 +0100
@@ -237,7 +237,8 @@
   def transitive_reduction_acyclic: Graph[Key, A] =
   {
     val trans = this.transitive_closure
-    assert(!trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+    if (trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+      error("Cyclic graph")
 
     var graph = this
     for {

--- a/src/Tools/jEdit/src/Isabelle.props	Mon Dec 10 15:13:13 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Mon Dec 10 15:17:47 2012 +0100
@@ -29,7 +29,6 @@
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu= \
-  isabelle.graphview-panel \
   isabelle.monitor-panel \
   isabelle.output-panel \
   isabelle.protocol-panel \
@@ -38,7 +37,6 @@
   isabelle.symbols-panel \
   isabelle.syslog-panel \
   isabelle.theories-panel
-isabelle.graphview-panel.label=Graphview panel
 isabelle.monitor-panel.label=Monitor panel
 isabelle.output-panel.label=Output panel
 isabelle.protocol-panel.label=Protocol panel
@@ -49,7 +47,6 @@
 isabelle.theories-panel.label=Theories panel
 
 #dockables
-isabelle-graphview.title=Graphview
 isabelle-info.title=Info
 isabelle-monitor.title=Monitor
 isabelle-output.title=Output

--- a/src/Tools/jEdit/src/actions.xml	Mon Dec 10 15:13:13 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Mon Dec 10 15:17:47 2012 +0100
@@ -22,11 +22,6 @@
 			wm.addDockableWindow("isabelle-output");
 		</CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.graphview-panel">
-		<CODE>
-			wm.addDockableWindow("isabelle-graphview");
-		</CODE>
-	</ACTION>
 	<ACTION NAME="isabelle.raw-output-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-raw-output");

--- a/src/Tools/jEdit/src/active.scala	Mon Dec 10 15:13:13 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala	Mon Dec 10 15:17:47 2012 +0100
@@ -26,31 +26,45 @@
           val buffer = model.buffer
           val snapshot = model.snapshot()
 
+          def try_replace_command(exec_id: Document.ID, s: String)
+          {
+            snapshot.state.execs.get(exec_id).map(_.command) match {
+              case Some(command) =>
+                snapshot.node.command_start(command) match {
+                  case Some(start) =>
+                    JEdit_Lib.buffer_edit(buffer) {
+                      buffer.remove(start, command.proper_range.length)
+                      buffer.insert(start, s)
+                    }
+                  case None =>
+                }
+              case None =>
+            }
+          }
+
           if (!snapshot.is_outdated) {
             elem match {
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
                   case Position.Id(exec_id) =>
-                    snapshot.state.execs.get(exec_id).map(_.command) match {
-                      case Some(command) =>
-                        snapshot.node.command_start(command) match {
-                          case Some(start) =>
-                            JEdit_Lib.buffer_edit(buffer) {
-                              buffer.remove(start, command.proper_range.length)
-                              buffer.insert(start, text)
-                            }
-                          case None =>
-                        }
-                      case None =>
-                    }
+                    try_replace_command(exec_id, text)
                   case _ =>
                     if (props.exists(_ == Markup.PADDING_LINE))
                       Isabelle.insert_line_padding(text_area, text)
                     else text_area.setSelectedText(text)
                 }
 
-              case XML.Elem(Markup(Markup.GRAPHVIEW, props), body) =>
-                java.lang.System.err.println("graphview " + props)  // FIXME
+              case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
+                try_replace_command(exec_id, "")
+                default_thread_pool.submit(() =>
+                  {
+                    val graph =
+                      Exn.capture {
+                        isabelle.graphview.Model.decode_graph(body)
+                          .transitive_reduction_acyclic
+                      }
+                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
+                  })
 
               case _ =>
             }

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 10 15:13:13 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 10 15:17:47 2012 +0100
@@ -1,8 +1,7 @@
 /*  Title:      Tools/jEdit/src/graphview_dockable.scala
-    Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
-Dockable window for graphview.
+Stateless dockable window for graphview.
 */
 
 package isabelle.jedit
@@ -10,133 +9,79 @@
 
 import isabelle._
 
-import java.awt.BorderLayout
-import javax.swing.{JPanel, JComponent}
-
-import scala.actors.Actor._
+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()
 
-
-  /* component state -- owned by Swing thread */
-
-  private val do_update = true  // FIXME
-
-  private var current_snapshot = Document.State.init.snapshot()
-  private var current_state = Command.empty.init_state
-  private var current_graph: XML.Body = Nil
-
-
-  /* GUI components */
-
-  private val graphview = new JPanel
-
-  // FIXME mutable GUI content
-  private def set_graphview(snapshot: Document.Snapshot, graph_xml: XML.Body)
-  {
-    val graph = isabelle.graphview.Model.decode_graph(graph_xml).transitive_reduction_acyclic
+  private val snapshot = Graphview_Dockable.implicit_snapshot
+  private val graph = Graphview_Dockable.implicit_graph
 
-    graphview.removeAll()
-    graphview.setLayout(new BorderLayout)
-    val panel =
-      new isabelle.graphview.Main_Panel(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, body)
-          null
-        }
-      }
-    graphview.add(panel.peer, BorderLayout.CENTER)
-    graphview.revalidate()
-  }
-
-  set_graphview(current_snapshot, current_graph)
-  set_content(graphview)
-
-
-  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
-  {
-    Swing_Thread.require()
+  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 (new_snapshot, new_state) =
-      Document_View(view.getTextArea) match {
-        case Some(doc_view) =>
-          val snapshot = doc_view.model.snapshot()
-          if (follow && !snapshot.is_outdated) {
-            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-              case Some(cmd) =>
-                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
-              case None =>
-                (Document.State.init.snapshot(), Command.empty.init_state)
-            }
+  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, body)
+            null
           }
-          else (current_snapshot, current_state)
-        case None => (current_snapshot, current_state)
-      }
-
-    val new_graph =
-      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
-        new_state.markup.cumulate[Option[XML.Body]](
-          new_state.command.range, None, Some(Set(Markup.GRAPHVIEW)),
-        {
-          case (_, Text.Info(_, XML.Elem(Markup(Markup.GRAPHVIEW, _), graph))) =>
-            Some(graph)
-        }).filter(_.info.isDefined) match {
-          case Text.Info(_, Some(graph)) #:: _ => graph
-          case _ => Nil
         }
-      }
-      else current_graph
-
-    if (new_graph != current_graph) set_graphview(new_snapshot, new_graph)
-
-    current_snapshot = new_snapshot
-    current_state = new_state
-    current_graph = new_graph
-  }
-
-
-  /* main actor */
-
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>  // FIXME
-
-        case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
-
-        case Session.Caret_Focus =>
-          Swing_Thread.later { handle_update(do_update, None) }
-
-        case bad =>
-          java.lang.System.err.println("Graphview_Dockable: ignoring bad message " + bad)
-      }
+      case Exn.Exn(exn) => new TextArea(Exn.message(exn))
     }
-  }
+  set_content(graphview)
 
   override def init()
   {
     Swing_Thread.require()
-
-    PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor
-    PIDE.session.caret_focus += main_actor
-    handle_update(do_update, None)
+    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   }
 
   override def exit()
   {
     Swing_Thread.require()
-
-    PIDE.session.global_options -= main_actor
-    PIDE.session.commands_changed -= main_actor
-    PIDE.session.caret_focus -= main_actor
+    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   }
 }