--- a/src/Pure/General/graph_display.ML Wed Sep 26 14:23:33 2012 +0200
+++ b/src/Pure/General/graph_display.ML Wed Sep 26 14:38:23 2012 +0200
@@ -57,8 +57,9 @@
fun display_graph graph =
if print_mode_active graphview_reportN then
- Output.report
- (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)))
+ (Output.report
+ (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)));
+ writeln "(see graphview)")
else
let
val browser =
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Sep 26 14:23:33 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Sep 26 14:38:23 2012 +0200
@@ -11,8 +11,8 @@
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
+ "src/graphview_dockable.scala"
"src/html_panel.scala"
- "src/graph_dockable.scala"
"src/hyperlink.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Wed Sep 26 14:23:33 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Sep 26 14:38:23 2012 +0200
@@ -40,10 +40,10 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graph-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
-isabelle.graph-panel.label=Graph panel
+isabelle.graphview-panel.label=Graphview panel
isabelle.output1-panel.label=Output1 panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
@@ -53,7 +53,7 @@
#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
-isabelle-graph.title=Graph
+isabelle-graphview.title=Graphview
isabelle-output1.title=Output1
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
--- a/src/Tools/jEdit/src/actions.xml Wed Sep 26 14:23:33 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml Wed Sep 26 14:38:23 2012 +0200
@@ -27,9 +27,9 @@
wm.addDockableWindow("isabelle-output1");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.graph-panel">
+ <ACTION NAME="isabelle.graphview-panel">
<CODE>
- wm.addDockableWindow("isabelle-graph");
+ wm.addDockableWindow("isabelle-graphview");
</CODE>
</ACTION>
<ACTION NAME="isabelle.raw-output-panel">
--- a/src/Tools/jEdit/src/dockables.xml Wed Sep 26 14:23:33 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Wed Sep 26 14:38:23 2012 +0200
@@ -14,8 +14,8 @@
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-graph" MOVABLE="TRUE">
- new isabelle.jedit.Graph_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
+ new isabelle.jedit.Graphview_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-output1" MOVABLE="TRUE">
new isabelle.jedit.Output1_Dockable(view, position);
--- a/src/Tools/jEdit/src/graph_dockable.scala Wed Sep 26 14:23:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-/* Title: Tools/jEdit/src/graph_dockable.scala
- Author: Markus Kaiser, TU Muenchen
- Author: Makarius
-
-Dockable window for graphview.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.BorderLayout
-import javax.swing.JPanel
-
-import scala.actors.Actor._
-
-import org.gjt.sp.jedit.View
-
-
-class Graph_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(graph: XML.Body)
- {
- graphview.removeAll()
- graphview.setLayout(new BorderLayout)
- val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
- graphview.add(panel.peer, BorderLayout.CENTER)
- }
-
- set_graphview(current_graph)
- set_content(graphview)
-
-
- private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
- {
- Swing_Thread.require()
-
- 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)
- }
- }
- 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(Isabelle_Markup.GRAPHVIEW)),
- {
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_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_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("Graph_Dockable: ignoring bad message " + bad)
- }
- }
- }
-
- override def init()
- {
- Swing_Thread.require()
-
- Isabelle.session.global_options += main_actor
- Isabelle.session.commands_changed += main_actor
- Isabelle.session.caret_focus += main_actor
- handle_update(do_update, None)
- }
-
- override def exit()
- {
- Swing_Thread.require()
-
- Isabelle.session.global_options -= main_actor
- Isabelle.session.commands_changed -= main_actor
- Isabelle.session.caret_focus -= main_actor
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Sep 26 14:38:23 2012 +0200
@@ -0,0 +1,131 @@
+/* Title: Tools/jEdit/src/graphview_dockable.scala
+ Author: Markus Kaiser, TU Muenchen
+ Author: Makarius
+
+Dockable window for graphview.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import javax.swing.JPanel
+
+import scala.actors.Actor._
+
+import org.gjt.sp.jedit.View
+
+
+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(graph: XML.Body)
+ {
+ graphview.removeAll()
+ graphview.setLayout(new BorderLayout)
+ val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
+ graphview.add(panel.peer, BorderLayout.CENTER)
+ }
+
+ set_graphview(current_graph)
+ set_content(graphview)
+
+
+ private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
+ {
+ Swing_Thread.require()
+
+ 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)
+ }
+ }
+ 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(Isabelle_Markup.GRAPHVIEW)),
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_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_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)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options += main_actor
+ Isabelle.session.commands_changed += main_actor
+ Isabelle.session.caret_focus += main_actor
+ handle_update(do_update, None)
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options -= main_actor
+ Isabelle.session.commands_changed -= main_actor
+ Isabelle.session.caret_focus -= main_actor
+ }
+}