src/Tools/jEdit/src/graph_dockable.scala
changeset 49566 66cbf8bb4693
parent 49557 61988f9df94d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/graph_dockable.scala	Tue Sep 25 22:36:06 2012 +0200
     1.3 @@ -0,0 +1,131 @@
     1.4 +/*  Title:      Tools/jEdit/src/graph_dockable.scala
     1.5 +    Author:     Markus Kaiser, TU Muenchen
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Dockable window for graphview.
     1.9 +*/
    1.10 +
    1.11 +package isabelle.jedit
    1.12 +
    1.13 +
    1.14 +import isabelle._
    1.15 +
    1.16 +import java.awt.BorderLayout
    1.17 +import javax.swing.JPanel
    1.18 +
    1.19 +import scala.actors.Actor._
    1.20 +
    1.21 +import org.gjt.sp.jedit.View
    1.22 +
    1.23 +
    1.24 +class Graph_Dockable(view: View, position: String) extends Dockable(view, position)
    1.25 +{
    1.26 +  Swing_Thread.require()
    1.27 +
    1.28 +
    1.29 +  /* component state -- owned by Swing thread */
    1.30 +
    1.31 +  private val do_update = true  // FIXME
    1.32 +
    1.33 +  private var current_snapshot = Document.State.init.snapshot()
    1.34 +  private var current_state = Command.empty.init_state
    1.35 +  private var current_graph: XML.Body = Nil
    1.36 +
    1.37 +
    1.38 +  /* GUI components */
    1.39 +
    1.40 +  private val graphview = new JPanel
    1.41 +
    1.42 +  // FIXME mutable GUI content
    1.43 +  private def set_graphview(graph: XML.Body)
    1.44 +  {
    1.45 +    graphview.removeAll()
    1.46 +    graphview.setLayout(new BorderLayout)
    1.47 +    val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
    1.48 +    graphview.add(panel.peer, BorderLayout.CENTER)
    1.49 +  }
    1.50 +
    1.51 +  set_graphview(current_graph)
    1.52 +  set_content(graphview)
    1.53 +
    1.54 +
    1.55 +  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    1.56 +  {
    1.57 +    Swing_Thread.require()
    1.58 +
    1.59 +    val (new_snapshot, new_state) =
    1.60 +      Document_View(view.getTextArea) match {
    1.61 +        case Some(doc_view) =>
    1.62 +          val snapshot = doc_view.model.snapshot()
    1.63 +          if (follow && !snapshot.is_outdated) {
    1.64 +            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
    1.65 +              case Some(cmd) =>
    1.66 +                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    1.67 +              case None =>
    1.68 +                (Document.State.init.snapshot(), Command.empty.init_state)
    1.69 +            }
    1.70 +          }
    1.71 +          else (current_snapshot, current_state)
    1.72 +        case None => (current_snapshot, current_state)
    1.73 +      }
    1.74 +
    1.75 +    val new_graph =
    1.76 +      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
    1.77 +        new_state.markup.cumulate[Option[XML.Body]](
    1.78 +          new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
    1.79 +        {
    1.80 +          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
    1.81 +            Some(graph)
    1.82 +        }).filter(_.info.isDefined) match {
    1.83 +          case Text.Info(_, Some(graph)) #:: _ => graph
    1.84 +          case _ => Nil
    1.85 +        }
    1.86 +      }
    1.87 +      else current_graph
    1.88 +
    1.89 +    if (new_graph != current_graph) set_graphview(new_graph)
    1.90 +
    1.91 +    current_snapshot = new_snapshot
    1.92 +    current_state = new_state
    1.93 +    current_graph = new_graph
    1.94 +  }
    1.95 +
    1.96 +
    1.97 +  /* main actor */
    1.98 +
    1.99 +  private val main_actor = actor {
   1.100 +    loop {
   1.101 +      react {
   1.102 +        case Session.Global_Options =>  // FIXME
   1.103 +
   1.104 +        case changed: Session.Commands_Changed =>
   1.105 +          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
   1.106 +
   1.107 +        case Session.Caret_Focus =>
   1.108 +          Swing_Thread.later { handle_update(do_update, None) }
   1.109 +
   1.110 +        case bad =>
   1.111 +          java.lang.System.err.println("Graph_Dockable: ignoring bad message " + bad)
   1.112 +      }
   1.113 +    }
   1.114 +  }
   1.115 +
   1.116 +  override def init()
   1.117 +  {
   1.118 +    Swing_Thread.require()
   1.119 +
   1.120 +    Isabelle.session.global_options += main_actor
   1.121 +    Isabelle.session.commands_changed += main_actor
   1.122 +    Isabelle.session.caret_focus += main_actor
   1.123 +    handle_update(do_update, None)
   1.124 +  }
   1.125 +
   1.126 +  override def exit()
   1.127 +  {
   1.128 +    Swing_Thread.require()
   1.129 +
   1.130 +    Isabelle.session.global_options -= main_actor
   1.131 +    Isabelle.session.commands_changed -= main_actor
   1.132 +    Isabelle.session.caret_focus -= main_actor
   1.133 +  }
   1.134 +}