src/Tools/jEdit/src/graph_dockable.scala
author wenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 49566 66cbf8bb4693
parent 49557 src/Tools/Graphview/src/dockable.scala@61988f9df94d
permissions -rw-r--r--
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
wenzelm@49566
     1
/*  Title:      Tools/jEdit/src/graph_dockable.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@49566
     3
    Author:     Makarius
markus@49557
     4
wenzelm@49566
     5
Dockable window for graphview.
markus@49557
     6
*/
markus@49557
     7
wenzelm@49566
     8
package isabelle.jedit
markus@49557
     9
markus@49557
    10
markus@49557
    11
import isabelle._
wenzelm@49566
    12
wenzelm@49566
    13
import java.awt.BorderLayout
wenzelm@49566
    14
import javax.swing.JPanel
markus@49557
    15
markus@49557
    16
import scala.actors.Actor._
markus@49557
    17
markus@49557
    18
import org.gjt.sp.jedit.View
markus@49557
    19
markus@49557
    20
wenzelm@49566
    21
class Graph_Dockable(view: View, position: String) extends Dockable(view, position)
markus@49557
    22
{
wenzelm@49566
    23
  Swing_Thread.require()
wenzelm@49566
    24
wenzelm@49566
    25
wenzelm@49566
    26
  /* component state -- owned by Swing thread */
wenzelm@49566
    27
wenzelm@49566
    28
  private val do_update = true  // FIXME
wenzelm@49566
    29
wenzelm@49566
    30
  private var current_snapshot = Document.State.init.snapshot()
wenzelm@49566
    31
  private var current_state = Command.empty.init_state
wenzelm@49566
    32
  private var current_graph: XML.Body = Nil
wenzelm@49566
    33
wenzelm@49566
    34
wenzelm@49566
    35
  /* GUI components */
wenzelm@49566
    36
wenzelm@49566
    37
  private val graphview = new JPanel
wenzelm@49566
    38
wenzelm@49566
    39
  // FIXME mutable GUI content
wenzelm@49566
    40
  private def set_graphview(graph: XML.Body)
wenzelm@49566
    41
  {
wenzelm@49566
    42
    graphview.removeAll()
wenzelm@49566
    43
    graphview.setLayout(new BorderLayout)
wenzelm@49566
    44
    val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
wenzelm@49566
    45
    graphview.add(panel.peer, BorderLayout.CENTER)
markus@49557
    46
  }
markus@49557
    47
wenzelm@49566
    48
  set_graphview(current_graph)
wenzelm@49566
    49
  set_content(graphview)
markus@49557
    50
wenzelm@49566
    51
wenzelm@49566
    52
  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
wenzelm@49566
    53
  {
wenzelm@49566
    54
    Swing_Thread.require()
wenzelm@49566
    55
wenzelm@49566
    56
    val (new_snapshot, new_state) =
wenzelm@49566
    57
      Document_View(view.getTextArea) match {
wenzelm@49566
    58
        case Some(doc_view) =>
wenzelm@49566
    59
          val snapshot = doc_view.model.snapshot()
wenzelm@49566
    60
          if (follow && !snapshot.is_outdated) {
wenzelm@49566
    61
            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
wenzelm@49566
    62
              case Some(cmd) =>
wenzelm@49566
    63
                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
wenzelm@49566
    64
              case None =>
wenzelm@49566
    65
                (Document.State.init.snapshot(), Command.empty.init_state)
wenzelm@49566
    66
            }
wenzelm@49566
    67
          }
wenzelm@49566
    68
          else (current_snapshot, current_state)
wenzelm@49566
    69
        case None => (current_snapshot, current_state)
wenzelm@49566
    70
      }
wenzelm@49566
    71
wenzelm@49566
    72
    val new_graph =
wenzelm@49566
    73
      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
wenzelm@49566
    74
        new_state.markup.cumulate[Option[XML.Body]](
wenzelm@49566
    75
          new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
wenzelm@49566
    76
        {
wenzelm@49566
    77
          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
wenzelm@49566
    78
            Some(graph)
wenzelm@49566
    79
        }).filter(_.info.isDefined) match {
wenzelm@49566
    80
          case Text.Info(_, Some(graph)) #:: _ => graph
wenzelm@49566
    81
          case _ => Nil
wenzelm@49566
    82
        }
wenzelm@49566
    83
      }
wenzelm@49566
    84
      else current_graph
wenzelm@49566
    85
wenzelm@49566
    86
    if (new_graph != current_graph) set_graphview(new_graph)
wenzelm@49566
    87
wenzelm@49566
    88
    current_snapshot = new_snapshot
wenzelm@49566
    89
    current_state = new_state
wenzelm@49566
    90
    current_graph = new_graph
wenzelm@49566
    91
  }
wenzelm@49566
    92
markus@49557
    93
markus@49557
    94
  /* main actor */
markus@49557
    95
markus@49557
    96
  private val main_actor = actor {
markus@49557
    97
    loop {
markus@49557
    98
      react {
wenzelm@49566
    99
        case Session.Global_Options =>  // FIXME
wenzelm@49566
   100
wenzelm@49566
   101
        case changed: Session.Commands_Changed =>
wenzelm@49566
   102
          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
wenzelm@49566
   103
wenzelm@49566
   104
        case Session.Caret_Focus =>
wenzelm@49566
   105
          Swing_Thread.later { handle_update(do_update, None) }
wenzelm@49566
   106
wenzelm@49566
   107
        case bad =>
wenzelm@49566
   108
          java.lang.System.err.println("Graph_Dockable: ignoring bad message " + bad)
markus@49557
   109
      }
markus@49557
   110
    }
markus@49557
   111
  }
markus@49557
   112
wenzelm@49566
   113
  override def init()
wenzelm@49566
   114
  {
wenzelm@49566
   115
    Swing_Thread.require()
wenzelm@49566
   116
wenzelm@49566
   117
    Isabelle.session.global_options += main_actor
wenzelm@49566
   118
    Isabelle.session.commands_changed += main_actor
wenzelm@49566
   119
    Isabelle.session.caret_focus += main_actor
wenzelm@49566
   120
    handle_update(do_update, None)
wenzelm@49566
   121
  }
wenzelm@49566
   122
wenzelm@49566
   123
  override def exit()
wenzelm@49566
   124
  {
wenzelm@49566
   125
    Swing_Thread.require()
wenzelm@49566
   126
wenzelm@49566
   127
    Isabelle.session.global_options -= main_actor
wenzelm@49566
   128
    Isabelle.session.commands_changed -= main_actor
wenzelm@49566
   129
    Isabelle.session.caret_focus -= main_actor
wenzelm@49566
   130
  }
markus@49557
   131
}