# HG changeset patch
# User wenzelm
# Date 1355149067 -3600
# Node ID bfb5964e3041a71f9ab2bfbdc21af43decddab0e
# Parent 2af559170d0793aa4bb71df6b89b803ce60b5ae7
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
diff -r 2af559170d07 -r bfb5964e3041 src/Pure/General/graph.scala
--- 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 {
diff -r 2af559170d07 -r bfb5964e3041 src/Tools/jEdit/src/Isabelle.props
--- 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
diff -r 2af559170d07 -r bfb5964e3041 src/Tools/jEdit/src/actions.xml
--- 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");
-
-
- wm.addDockableWindow("isabelle-graphview");
-
-
wm.addDockableWindow("isabelle-raw-output");
diff -r 2af559170d07 -r bfb5964e3041 src/Tools/jEdit/src/active.scala
--- 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 _ =>
}
diff -r 2af559170d07 -r bfb5964e3041 src/Tools/jEdit/src/graphview_dockable.scala
--- 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))
}
}