# HG changeset patch
# User wenzelm
# Date 1349721597 -7200
# Node ID 30e2f3f1c6232f1f5e71eaa1874d8f24124a86f6
# Parent  15e1549e6afe9072e6a8249d8810332a45a7df26
more precise repaint and revalidate -- the latter is important to keep in sync with content update;

diff -r 15e1549e6afe -r 30e2f3f1c623 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Mon Oct 08 14:49:04 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Mon Oct 08 20:39:57 2012 +0200
@@ -54,9 +54,15 @@
     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() = visualizer.Coordinates.layout()  
@@ -74,7 +80,6 @@
       }  
     
     override def paint(g: Graphics2D) {
-      set_preferred_size()
       super.paintComponent(g)
       g.transform(Transform())
       
diff -r 15e1549e6afe -r 30e2f3f1c623 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Oct 08 14:49:04 2012 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Oct 08 20:39:57 2012 +0200
@@ -37,7 +37,7 @@
   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)
@@ -45,15 +45,16 @@
       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(current_snapshot, Isabelle.options.value)
+          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)
 
 
@@ -91,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