# HG changeset patch
# User wenzelm
# Date 1349776266 -7200
# Node ID fb88f0e4c710c867ac5b7aba51053ce24ae61744
# Parent  6f02b893dd87338bb9661ceb7459f7260de9e968# Parent  dd6fc7c9504a7269186e521c374008ffc5282ea8
merged

diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/lib/Tools/graphview
--- a/src/Tools/Graphview/lib/Tools/graphview	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Tue Oct 09 11:51:06 2012 +0200
@@ -8,7 +8,6 @@
 ## sources
 
 declare -a SOURCES=(
-  "src/floating_dialog.scala"
   "src/graph_panel.scala"
   "src/graphview.scala"
   "src/layout_pendulum.scala"
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/floating_dialog.scala
--- a/src/Tools/Graphview/src/floating_dialog.scala	Tue Oct 09 00:40:33 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/*  Title:      Tools/Graphview/src/floating_dialog.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-PopUp Dialog containing node meta-information.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import scala.swing.{Dialog, BorderPanel, Component, TextArea}
-import java.awt.{Font, Point, Dimension}
-
-
-class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
-extends Dialog
-{    
-  location = _location
-  title = _title
-  //No adaptive size because we don't want to resize the Dialog about 1 sec
-  //after it is shown.
-  preferredSize = new Dimension(300, 300)
-  peer.setAlwaysOnTop(true)
-
-  private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
-  private val text = new TextArea
-  text.peer.setFont(text_font)
-  text.editable = false
-
-  contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
-  text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
-}
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -10,31 +10,66 @@
 
 import java.awt.{Dimension, Graphics2D, Point, Rectangle}
 import java.awt.geom.{AffineTransform, Point2D}
-import javax.swing.ToolTipManager
+import java.awt.image.BufferedImage
+import javax.swing.{JScrollPane, JComponent}
+
 import scala.swing.{Panel, ScrollPane}
 import scala.swing.event._
 
 
-class Graph_Panel(private val vis: Visualizer) extends ScrollPane {
-  this.peer.setWheelScrollingEnabled(false)
+class Graph_Panel(
+    val visualizer: Visualizer,
+    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
+  extends ScrollPane
+{
+  panel =>
+
+  tooltip = ""
+
+  override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
+    override def getToolTipText(event: java.awt.event.MouseEvent): String =
+      node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+        case Some(name) =>
+          visualizer.model.complete.get_node(name).content match {
+            case Nil => null
+            case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+          }
+        case None => null
+      }
+  }
+
+  peer.setWheelScrollingEnabled(false)
   focusable = true
   requestFocus()
   
   horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  
-  def visualizer = vis
-  
+
+  private val gfx_aux =
+    new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
+  gfx_aux.setFont(visualizer.Font())
+  gfx_aux.setRenderingHints(visualizer.rendering_hints)
+
+  def node(at: Point2D): Option[String] =
+    visualizer.model.visible_nodes()
+      .find(name => visualizer.Drawer.shape(gfx_aux, Some(name)).contains(at))
+
+  def refresh()
+  {
+    paint_panel.set_preferred_size()
+    paint_panel.repaint()
+  }
+
   def fit_to_window() = {
     Transform.fit_to_window()
-    repaint()
+    refresh()
   }
   
-  def apply_layout() = vis.Coordinates.layout()  
+  def apply_layout() = visualizer.Coordinates.layout()  
 
   private val paint_panel = new Panel {    
     def set_preferred_size() {
-        val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
         val s = Transform.scale
         val (px, py) = Transform.padding
 
@@ -45,11 +80,10 @@
       }  
     
     override def paint(g: Graphics2D) {
-      set_preferred_size()
       super.paintComponent(g)
       g.transform(Transform())
       
-      vis.Drawer.paint_all_visible(g, true)
+      visualizer.Drawer.paint_all_visible(g, true)
     }
   }
   contents = paint_panel
@@ -68,21 +102,9 @@
       case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
       case MouseMoved(_, _, _) => repaint()
     }
-  private val r = {
-    import scala.actors.Actor._
-    
-    actor {
-      loop {
-        react {
-          // FIXME Swing thread!?
-          case _ => repaint()
-        }
-      }
-    }
-  }
-  vis.model.Colors.events += r
-  vis.model.Mutators.events += r
-  ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
+
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
   
   apply_layout()
   fit_to_window()
@@ -98,7 +120,7 @@
                 }
                 
     def apply() = {
-      val (minX, minY, _, _) = vis.Coordinates.bounds()
+      val (minX, minY, _, _) = visualizer.Coordinates.bounds()
       
       val at = AffineTransform.getScaleInstance(scale, scale)
       at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
@@ -106,10 +128,10 @@
     }
     
     def fit_to_window() {
-      if (vis.model.visible_nodes().isEmpty)
+      if (visualizer.model.visible_nodes().isEmpty)
         scale = 1
       else {
-        val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
 
         val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
         val (sx, sy) = (1d * size.width / dx, 1d * size.height / dy)
@@ -126,7 +148,6 @@
     }
   }
   
-  private val panel = this
   object Interaction {
     object Keyboard {
       import scala.swing.event.Key._
@@ -149,7 +170,7 @@
         }
         
         case('1', _) => {
-            vis.Coordinates.layout()
+            visualizer.Coordinates.layout()
         }
 
         case('2', _) => {
@@ -161,16 +182,11 @@
     }
     
     object Mouse {
-      import java.awt.image.BufferedImage
       import scala.swing.event.Key.Modifier._
       type Modifiers = Int
       type Dummy = ((String, String), Int)
       
       private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
-      private val g =
-        new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
-      g.setFont(vis.Font())
-      g.setRenderingHints(vis.rendering_hints)
 
       val react: PartialFunction[Event, Unit] = {   
         case MousePressed(_, p, _, _, _) => pressed(p)
@@ -181,41 +197,24 @@
           }
         case MouseWheelMoved(_, p, _, r) => wheel(r, p)
         case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
-        case MouseMoved(_, p, _) => moved(p)
       }
       
-      def node(at: Point2D): Option[String] = 
-        vis.model.visible_nodes().find({
-            l => vis.Drawer.shape(g, Some(l)).contains(at)
-          })
-      
       def dummy(at: Point2D): Option[Dummy] =
-        vis.model.visible_edges().map({
-            i => vis.Coordinates(i).zipWithIndex.map((i, _))
+        visualizer.model.visible_edges().map({
+            i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
           }).flatten.find({
             case (_, ((x, y), _)) => 
-              vis.Drawer.shape(g, None).contains(at.getX() - x, at.getY() - y)
+              visualizer.Drawer.shape(gfx_aux, None).contains(at.getX() - x, at.getY() - y)
           }) match {
             case None => None
             case Some((name, (_, index))) => Some((name, index))
           }
       
-      def moved(at: Point) {
-        val c = Transform.pane_to_graph_coordinates(at)
-        node(c) match {
-          case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
-          case None => panel.tooltip = null
-        }
-      }
-      
       def pressed(at: Point) {
         val c = Transform.pane_to_graph_coordinates(at)
         val l = node(c) match {
-          case Some(l) => if (vis.Selection(l))
-                            vis.Selection()
-                          else
-                            List(l)
-          
+          case Some(l) =>
+            if (visualizer.Selection(l)) visualizer.Selection() else List(l)
           case None => Nil
         }
         val d = l match {
@@ -238,43 +237,25 @@
         
         def left_click() {
           (p, m) match {
-            case (Some(l), Control) => vis.Selection.add(l)
+            case (Some(l), Control) => visualizer.Selection.add(l)
             case (None, Control) =>
 
-            case (Some(l), Shift) => vis.Selection.add(l)
+            case (Some(l), Shift) => visualizer.Selection.add(l)
             case (None, Shift) =>
 
-            case (Some(l), _) => vis.Selection.set(List(l))
-            case (None, _) => vis.Selection.clear
+            case (Some(l), _) => visualizer.Selection.set(List(l))
+            case (None, _) => visualizer.Selection.clear
           }          
         }
         
         def right_click() {
-          val menu = Popups(panel, p, vis.Selection())
+          val menu = Popups(panel, p, visualizer.Selection())
           menu.show(panel.peer, at.x, at.y)
         }
         
-        def double_click() {
-          p match {
-            case Some(l) => {
-                val p = at.clone.asInstanceOf[Point]
-                SwingUtilities.convertPointToScreen(p, panel.peer)
-                new Floating_Dialog(
-                  vis.Tooltip.content(l),
-                  vis.Caption(l),
-                  at
-                ).open
-            }
-            
-            case None =>
-          }          
-        }
-        
         if (clicks < 2) {
           if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
           else left_click()
-        } else if (clicks == 2) {
-          if (SwingUtilities.isLeftMouseButton(e.peer)) double_click()
         }
       }   
 
@@ -292,10 +273,10 @@
           }
             
           case (Nil, ds) =>
-            ds.foreach(d => vis.Coordinates.translate(d, (dx / s, dy / s)))
+            ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
                      
           case (ls, _) =>
-            ls.foreach(l => vis.Coordinates.translate(l, (dx / s, dy / s)))
+            ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
         }
       }
 
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -12,6 +12,7 @@
 import java.awt.Dimension
 import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
 import javax.swing.border.EmptyBorder
+import javax.swing.ToolTipManager
 
 
 object Graphview extends SwingApplication
@@ -24,6 +25,7 @@
         Platform.init_laf()
         Isabelle_System.init()
         Isabelle_System.install_fonts()
+        ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
 
         args.toList match {
           case List(arg) =>
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/layout_pendulum.scala
--- a/src/Tools/Graphview/src/layout_pendulum.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -22,12 +22,15 @@
   val x_distance = 350
   val y_distance = 350
   val pendulum_iterations = 10
+  val minimize_crossings_iterations = 40
   
-  def apply(graph: Model.Graph): Layout = {
-    if (graph.entries.isEmpty)
+  def apply(graph: Model.Graph): Layout =
+  {
+    if (graph.is_empty)
       (Map[Key, Point](), Map[(Key, Key), List[Point]]())
     else {
-      val (dummy_graph, dummies, dummy_levels) = {
+      val (dummy_graph, dummies, dummy_levels) =
+      {
         val initial_levels = level_map(graph)
 
         def add_dummies(graph: Model.Graph, from: Key, to: Key,
@@ -79,7 +82,7 @@
                 initial_coordinates(levels)
         )
 
-      val dummy_coords = 
+      val dummy_coords =
         (Map[(Key, Key), List[Point]]() /: dummies.keys) {
           case (map, key) => map + (key -> dummies(key).map(coords(_)))
         }
@@ -87,32 +90,30 @@
       (coords, dummy_coords)
     }
   }
-  
+
   def level_map(graph: Model.Graph): Map[Key, Int] = 
-    (Map[Key, Int]() /: graph.topological_order){
+    (Map[Key, Int]() /: graph.topological_order) {
       (levels, key) => {
-        val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
-        levels + (key -> (pred_levels.max + 1))
-      }}
+        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
+        levels + (key -> lev)
+      }
+    }
   
   def level_list(map: Map[Key, Int]): Levels =
-    (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
-        case ((key, i), list) => {
-            if (list.isEmpty) (i, List(key)) :: list
-            else {
-              val (j, l) = list.head
-              if (i == j) (i, key :: l) :: list.tail
-              else (i, List(key)) :: list
-            }
-        }
-    }.map(_._2)
-  
+  {
+    val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
+    val buckets = new Array[Level](max_lev + 1)
+    for (l <- 0 to max_lev) { buckets(l) = Nil }
+    for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
+    buckets.iterator.map(_.sorted).toList
+  }
+
   def count_crossings(graph: Model.Graph, levels: Levels): Int = {
     def in_level(ls: Levels): Int = ls match {
       case List(top, bot) =>
         top.zipWithIndex.map{
           case (outer_parent, outer_parent_index) => 
-            graph.imm_succs(outer_parent).map(bot.indexOf(_))
+            graph.imm_succs(outer_parent).map(bot.indexOf(_))  // FIXME iterator
             .map(outer_child => {
               (0 until outer_parent_index)
               .map(inner_parent => 
@@ -153,11 +154,11 @@
         }
       }
     
-    ((levels, count_crossings(graph, levels), true) /: (1 to 40)) {
+    ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
       case ((old_levels, old_crossings, top_down), _) => {
           val new_levels = resort(old_levels, top_down)
           val new_crossings = count_crossings(graph, new_levels)
-          if ( new_crossings < old_crossings)
+          if (new_crossings < old_crossings)
             (new_levels, new_crossings, !top_down)
           else
             (old_levels, old_crossings, !top_down)
@@ -250,7 +251,7 @@
     val regions = levels.map(level => level.map(new Region(graph, _)))
     
     ((regions, coords, true, true) /: (1 to pendulum_iterations)) {
-      case ((regions, coords, top_down, moved), _) => 
+      case ((regions, coords, top_down, moved), i) =>
         if (moved) {
           val (nextr, nextc, m) = iteration(regions, coords, top_down)
           (nextr, nextc, !top_down, m)
@@ -272,7 +273,7 @@
     
     def deflection(coords: Coordinates, use_preds: Boolean) = 
       nodes.map(k => (coords(k)._1,
-                      if (use_preds) graph.imm_preds(k).toList
+                      if (use_preds) graph.imm_preds(k).toList  // FIXME iterator
                       else graph.imm_succs(k).toList))
       .map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
       .sum / nodes.length
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -12,20 +12,31 @@
 
 import scala.collection.JavaConversions._
 import scala.swing.{BorderPanel, Button, BoxPanel,
-                    Orientation, Swing, CheckBox, Action, FileChooser}
+  Orientation, Swing, CheckBox, Action, FileChooser}
+
+import java.io.File
+import java.awt.{Color, Dimension}
+import java.awt.geom.Rectangle2D
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
 import javax.swing.border.EmptyBorder
-import java.awt.Dimension
-import java.io.File
+import javax.swing.JComponent
 
 
-class Main_Panel(graph: Model.Graph) extends BorderPanel
+class Main_Panel(graph: Model.Graph)
+  extends BorderPanel
 {
+  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+    "<html><pre style=\"font-family: " + Parameters.font_family +
+      "; font-size: " + Parameters.tooltip_font_size + "px; \">" +
+      HTML.encode(Pretty.string_of(body)) + "</pre></html>"
+
   focusable = true
   requestFocus()
   
   val model = new Model(graph)
   val visualizer = new Visualizer(model)
-  val graph_panel = new Graph_Panel(visualizer)
+  val graph_panel = new Graph_Panel(visualizer, make_tooltip)
   
   listenTo(keys)
   reactions += graph_panel.reactions
@@ -107,11 +118,6 @@
   add(options_panel, BorderPanel.Position.North)
   
   private def export(file: File) {
-    import java.awt.image.BufferedImage
-    import javax.imageio.ImageIO
-    import java.awt.geom.Rectangle2D
-    import java.awt.Color    
-    
     val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
     val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
                                 (math.abs(maxY - minY) + 200).toInt,
@@ -124,10 +130,7 @@
     visualizer.Drawer.paint_all_visible(g, false)
     g.dispose()    
     
-    try {
-      ImageIO.write(img, "png", file)
-    } catch {
-      case ex: Exception => ex.printStackTrace
-    }  
+    try { ImageIO.write(img, "png", file) }
+    catch { case ex: Exception => ex.printStackTrace }  // FIXME !?
   }
 }
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/model.scala
--- a/src/Tools/Graphview/src/model.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/model.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -10,14 +10,12 @@
 import isabelle._
 import isabelle.graphview.Mutators._
 import java.awt.Color
-import scala.actors.Actor
-import scala.actors.Actor._
 
 
 class Mutator_Container(val available: List[Mutator]) {
     type Mutator_Markup = (Boolean, Color, Mutator)
     
-    val events = new Event_Bus[Mutator_Event.Message]
+    val events = new Mutator_Event.Bus
     
     private var _mutators : List[Mutator_Markup] = Nil
     def apply() = _mutators
@@ -80,7 +78,7 @@
   def visible_nodes(): Iterator[String] = current.keys
   
   def visible_edges(): Iterator[(String, String)] =
-    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
+    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator
   
   def complete = graph
   def current: Model.Graph =
@@ -103,11 +101,5 @@
           }
     })
   }
-  Colors.events += actor {
-    loop {
-      react {
-        case _ => build_colors()
-      }
-    }
-  }
+  Colors.events += { case _ => build_colors() }
 }
\ No newline at end of file
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/mutator.scala
--- a/src/Tools/Graphview/src/mutator.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -139,7 +139,7 @@
     "Hide transitive edges",
     "Hides all transitive edges.",
     (g, s, d) => {
-      !g.imm_succs(s).filter(_ != d)
+      !g.imm_succs(s).filter(_ != d)  // FIXME iterator
       .exists(p => !(g.irreducible_paths(p, d).isEmpty))
     }
   )
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/mutator_dialog.scala
--- a/src/Tools/Graphview/src/mutator_dialog.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_dialog.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -14,16 +14,15 @@
 import javax.swing.border.EmptyBorder
 import scala.collection.JavaConversions._
 import scala.swing._
-import scala.actors.Actor
-import scala.actors.Actor._
 import isabelle.graphview.Mutators._
 import scala.swing.event.ValueChanged
 
 
 class Mutator_Dialog(
-  container: Mutator_Container, caption: String,
-  reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
-extends Dialog
+    container: Mutator_Container, caption: String,
+    reverse_caption: String = "Inverse",
+    show_color_chooser: Boolean = true)
+  extends Dialog
 {
   type Mutator_Markup = (Boolean, Color, Mutator)
   
@@ -36,15 +35,9 @@
     paintPanels
   }
 
-  container.events += actor {
-    loop {
-      react {
-        case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
-        case Mutator_Event.NewList(ms) => {
-            panels = getPanels(ms)
-        }
-      }
-    }
+  container.events += {
+    case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+    case Mutator_Event.NewList(ms) => panels = getPanels(ms)
   }
 
   override def open() {
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/mutator_event.scala
--- a/src/Tools/Graphview/src/mutator_event.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -7,14 +7,29 @@
 package isabelle.graphview
 
 
+import isabelle._
+
+import scala.collection.mutable
+
 import java.awt.Color
 
 
 object Mutator_Event
 {
   type Mutator_Markup = (Boolean, Color, Mutator)
-  
+
   sealed abstract class Message
   case class Add(m: Mutator_Markup) extends Message
   case class NewList(m: List[Mutator_Markup]) extends Message
+
+  type Receiver = PartialFunction[Message, Unit]
+
+  class Bus
+  {
+    private val receivers = new mutable.ListBuffer[Receiver]
+
+    def += (r: Receiver) { Swing_Thread.require(); receivers += r }
+    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
+    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+  }
 }
\ No newline at end of file
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/parameters.scala
--- a/src/Tools/Graphview/src/parameters.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/parameters.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -15,6 +15,8 @@
 {
   val font_family: String = "IsabelleText"
   val font_size: Int = 16
+  val tooltip_font_size: Int = 10
+
 
   object Colors {
     val Filter_Colors = List(
@@ -40,6 +42,6 @@
     val No_Axioms = Color.LIGHT_GRAY
   }
   
-  var long_names = true
+  var long_names = false
   var arrow_heads = false
 }
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/popups.scala
--- a/src/Tools/Graphview/src/popups.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/popups.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -61,9 +61,9 @@
 
 
         if (edges) {
-          val outs = ls.map(l => (l, curr.imm_succs(l)))
+          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
                       .filter(_._2.size > 0).sortBy(_._1)
-          val ins = ls.map(l => (l, curr.imm_preds(l)))
+          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
                       .filter(_._2.size > 0).sortBy(_._1)
 
           if (outs.nonEmpty || ins.nonEmpty) {
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -9,6 +9,7 @@
 import isabelle._
 
 import java.awt.{RenderingHints, Graphics2D}
+import javax.swing.JComponent
 
 
 class Visualizer(val model: Model) {
@@ -136,23 +137,9 @@
   }  
   
   object Caption {    
-    def apply(k: String) =
-      if (Parameters.long_names) k
-      else  k.split('.').last
-  }
-  
-  object Tooltip {
-    def content(name: String): XML.Body = model.complete.get_node(name).content
-
-    def text(name: String, fm: java.awt.FontMetrics): String = // null
-    {
-      val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
-      if (txt == "") null
-      else
-        "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
-            Parameters.font_size + "px; \">" +  // FIXME proper scaling (!?)
-          HTML.encode(txt) + "</pre></html>"
-    }
+    def apply(key: String) =
+      if (Parameters.long_names) key
+      else model.complete.get_node(key).name
   }
   
   object Font {
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -11,7 +11,7 @@
 import isabelle._
 
 import java.awt.BorderLayout
-import javax.swing.JPanel
+import javax.swing.{JPanel, JComponent}
 
 import scala.actors.Actor._
 
@@ -37,15 +37,24 @@
   private val graphview = new JPanel
 
   // FIXME mutable GUI content
-  private def set_graphview(graph: XML.Body)
+  private def set_graphview(snapshot: Document.Snapshot, graph: XML.Body)
   {
     graphview.removeAll()
     graphview.setLayout(new BorderLayout)
-    val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
+    val panel =
+      new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
+        override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+        {
+          val rendering = Isabelle_Rendering(snapshot, Isabelle.options.value)
+          new Pretty_Tooltip(view, parent, rendering, x, y, body)
+          null
+        }
+      }
     graphview.add(panel.peer, BorderLayout.CENTER)
+    graphview.revalidate()
   }
 
-  set_graphview(current_graph)
+  set_graphview(current_snapshot, current_graph)
   set_content(graphview)
 
 
@@ -83,7 +92,7 @@
       }
       else current_graph
 
-    if (new_graph != current_graph) set_graphview(new_graph)
+    if (new_graph != current_graph) set_graphview(new_snapshot, new_graph)
 
     current_snapshot = new_snapshot
     current_state = new_state
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -23,10 +23,10 @@
 
 class Pretty_Tooltip(
   view: View,
-  text_area: TextArea,
+  parent: JComponent,
   rendering: Isabelle_Rendering,
   mouse_x: Int, mouse_y: Int, body: XML.Body)
-  extends JWindow(JEdit_Lib.parent_window(text_area) getOrElse view)
+  extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
 {
   window =>
 
@@ -115,10 +115,8 @@
   }
 
   {
-    val container = text_area.getPainter
-    val font_metrics = container.getFontMetrics
-    val point = new Point(mouse_x, mouse_y + font_metrics.getHeight / 2)
-    SwingUtilities.convertPointToScreen(point, container)
+    val point = new Point(mouse_x, mouse_y)
+    SwingUtilities.convertPointToScreen(point, parent)
 
     val screen = Toolkit.getDefaultToolkit.getScreenSize
     val x = point.x min (screen.width - window.getWidth)
diff -r 6f02b893dd87 -r fb88f0e4c710 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Oct 09 11:51:06 2012 +0200
@@ -205,7 +205,11 @@
           val tip =
             if (control) rendering.tooltip(range)
             else rendering.tooltip_message(range)
-          if (!tip.isEmpty) new Pretty_Tooltip(view, text_area, rendering, x, y, tip)
+          if (!tip.isEmpty) {
+            val painter = text_area.getPainter
+            val y1 = y + painter.getFontMetrics.getHeight / 2
+            new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+          }
         }
         null
       }