# HG changeset patch # User wenzelm # Date 1348663103 -7200 # Node ID 2265456f6131202bbd439451678e049ed9b2b38d # Parent 7b6aaf446496065e91e6e69734fec3f40761e935 more uniform graphview terminology; diff -r 7b6aaf446496 -r 2265456f6131 src/Pure/General/graph_display.ML --- 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 = diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/src/actions.xml --- 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"); - + - wm.addDockableWindow("isabelle-graph"); + wm.addDockableWindow("isabelle-graphview"); diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/src/dockables.xml --- 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 @@ new isabelle.jedit.Output_Dockable(view, position); - - new isabelle.jedit.Graph_Dockable(view, position); + + new isabelle.jedit.Graphview_Dockable(view, position); new isabelle.jedit.Output1_Dockable(view, position); diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/src/graph_dockable.scala --- 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 - } -} diff -r 7b6aaf446496 -r 2265456f6131 src/Tools/jEdit/src/graphview_dockable.scala --- /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 + } +}