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