# HG changeset patch
# User immler@in.tum.de
# Date 1225633826 -3600
# Node ID aa4f35a305fa603758f3eaa1d7fc5117bc9d44af
# Parent  1714aeef838840714e82b7350201e47550365a3f
calculate preferred sizes only when needed

diff -r 1714aeef8388 -r aa4f35a305fa src/Tools/jEdit/build.xml
--- a/src/Tools/jEdit/build.xml	Sun Nov 02 14:32:18 2008 +0100
+++ b/src/Tools/jEdit/build.xml	Sun Nov 02 14:50:26 2008 +0100
@@ -72,4 +72,7 @@
       <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
       <copy file="plugin/IsabellePlugin.props" todir="${build.classes.dir}" />
     </target>
+    <target name="-post-jar">
+      <copy file="${dist.jar}" todir="/Users/fabian/tum/hiwi/jedit/jedit-sources/jEdit/build/jars/" />
+    </target>
 </project>
diff -r 1714aeef8388 -r aa4f35a305fa src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml	Sun Nov 02 14:32:18 2008 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml	Sun Nov 02 14:50:26 2008 +0100
@@ -10,6 +10,6 @@
 		new isabelle.jedit.StateViewDockable(view, position);
 	</DOCKABLE>
 	<DOCKABLE NAME="Isabelle_scroller">
-		new isabelle.jedit.LazyScroller(view, position);
+		new isabelle.jedit.ScrollerDockable(view, position);
 	</DOCKABLE>
 </DOCKABLES>
\ No newline at end of file
diff -r 1714aeef8388 -r aa4f35a305fa src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Nov 02 14:32:18 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Nov 02 14:50:26 2008 +0100
@@ -100,17 +100,21 @@
   //add panel to the cache
   def add_to_cache (message_no: Int, panel: XHTMLPanel) = {
     message_cache = message_cache.update (message_no, panel)
-    calculate_preferred_size(panel)
-    System.err.println("Added " + message_no + " with preferred Size " + panel.getPreferredSize + " to cache")
   }
   
   //render and load a message into cache, place its bottom at y-coordinate;
   def set_message (message_no: Int, y: Int) = {
     //get or add panel from/to cache
     if(!message_cache.isDefinedAt(message_no)){
-      add_to_cache (message_no, render (message_buffer(message_no)))
+      if(message_buffer.isDefinedAt(message_no)){
+        add_to_cache (message_no, render (message_buffer(message_no)))
+      }
     }
     val panel = message_cache.get(message_no).get
+    // recalculate preferred sie after resizing
+    if(panel.getPreferredSize.getWidth.toInt != message_view.getWidth)
+      calculate_preferred_size (panel)
+    //place message on view
     val width = panel.getPreferredSize.getWidth.toInt
     val height = panel.getPreferredSize.getHeight.toInt
     panel.setBounds(0, y - height, width, height)
@@ -147,14 +151,6 @@
   override def componentHidden(e: ComponentEvent){}
   override def componentMoved(e: ComponentEvent){}
   override def componentResized(e: ComponentEvent){
-    // remove all hidden messages from cache
-    // TODO: move to unlayouted cache
-    message_cache = message_cache filter ( pair => pair match {case (no, _) =>
-      no <= message_no && no >= message_no - message_view.getComponents.length})
-    //calculate preferred size for each panel
-    message_cache foreach (pair => pair match { case (_, pa) =>
-      calculate_preferred_size (pa)
-    })
     update_view
   }