# HG changeset patch
# User immler@in.tum.de
# Date 1225221328 -3600
# Node ID 3775958051c56886813c7f399932bde4319c1c8c
# Parent  4a3bdb561d11c4fff273073fe65cbcc026e5535c
absolute positioning according to preferred size of panels,
scrolling one message per unit
rendered messages are cached

diff -r 4a3bdb561d11 -r 3775958051c5 src/Tools/jEdit/build.xml
--- a/src/Tools/jEdit/build.xml	Sun Oct 26 00:10:39 2008 +0200
+++ b/src/Tools/jEdit/build.xml	Tue Oct 28 20:15:28 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 4a3bdb561d11 -r 3775958051c5 src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml	Sun Oct 26 00:10:39 2008 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml	Tue Oct 28 20:15:28 2008 +0100
@@ -10,6 +10,6 @@
 		new isabelle.jedit.StateViewDockable(view, position);
 	</DOCKABLE>
 	<DOCKABLE NAME="Isabelle_scroller">
-		new isabelle.jedit.XMLScroller(view, position);
+		new isabelle.jedit.LazyScroller(view, position);
 	</DOCKABLE>
 </DOCKABLES>
\ No newline at end of file
diff -r 4a3bdb561d11 -r 3775958051c5 src/Tools/jEdit/src/jedit/LazyScroller.scala
--- a/src/Tools/jEdit/src/jedit/LazyScroller.scala	Sun Oct 26 00:10:39 2008 +0200
+++ b/src/Tools/jEdit/src/jedit/LazyScroller.scala	Tue Oct 28 20:15:28 2008 +0100
@@ -9,11 +9,10 @@
 import java.io.{ ByteArrayInputStream, FileInputStream, InputStream }
 
 import scala.collection.mutable.ArrayBuffer
-import scala.collection.jcl.ArrayList
 
 import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar }
 import java.awt.image.BufferedImage
-import java.awt.event.{ AdjustmentListener, AdjustmentEvent }
+import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
 import javax.swing.{ JScrollBar, JPanel, JScrollPane, ScrollPaneConstants }
 
 import isabelle.IsabelleSystem.getenv
@@ -48,98 +47,123 @@
 }
 
 
-abstract class LazyScroller[T] extends JPanel with AdjustmentListener{
+class LazyScroller(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener {
   //holding the unrendered messages
-  val message_buffer = new ArrayBuffer[T]()
+  val message_buffer = new ArrayBuffer[Document]()
+  //rendered messages
+  var message_cache = Map[Int, XHTMLPanel]()
   // defining the current view
-  val scrollunit = 10 //TODO: not used
-  var message_offset = 0 //TODO: not used; how many pixels of the topmost message are hidden
-  var message_no = 0  //index of the topmost message
-  var message_view = new JPanel
-  message_view.setLayout(new GridLayout(1,1))
+  val scrollunit = 10 
+  var message_offset = 0 //how many pixels of the lowest message are hidden
+  var message_no = -1  //index of the lowest message
+  // absolute positioning for messages
+  val message_view = new JPanel
+  message_view.setLayout(null)
   // setting up view
   setLayout(new BorderLayout())
   val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1)
   vscroll.addAdjustmentListener(this)
   add (vscroll, BorderLayout.EAST)
   add (message_view, BorderLayout.CENTER)
+  addComponentListener(this)
 
 
-  // subclasses should implement this
-  def render (message : T) : JPanel
+  //Render a message to a Panel
+  def render (message: Document): XHTMLPanel = {
+    val panel = new XHTMLPanel(new UserAgent())
+
+    val fontResolver =
+      panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
+    if (Plugin.plugin.viewFont != null)
+      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+    Plugin.plugin.viewFontChanged.add(font => {
+      if (Plugin.plugin.viewFont != null)
+        fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+      panel.relayout()
+    })
 
-  //TODO: - add more than one message
-  //      - render only when necessary
+    panel.setDocument(message, LazyScroller.baseURL)
+    panel
+  }
+  
+  //calculates preferred size of panel and add it to the cache and view
+  def add_to_cache (message_no: Int, panel: XHTMLPanel) = {
+    message_cache = message_cache.update (message_no, panel)
+    //necessary for calculating preferred size of panel
+    message_view.add (panel)
+    panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width
+    panel.doLayout (panel.getGraphics) //lay out, preferred size is set then
+    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)))
+    }
+    val panel = message_cache.get(message_no).get
+    val width = panel.getPreferredSize.getWidth.toInt
+    val height = panel.getPreferredSize.getHeight.toInt
+    panel.setBounds(0, y - height, width, height)
+    message_view.add(panel)
+    panel
+  }
+  
   def update_view = {
     message_view.removeAll()
-    val rendered_message = render (message_buffer(message_no))
-    val resizable = new JScrollPane(rendered_message, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER)
-    message_view.add (resizable)
-  }
-  
-  def update_scrollbar = {
-    vscroll.setValue (message_no)
-    vscroll.setMaximum (Math.max(1, message_buffer.length))
+    var n = message_no
+    var y:Int = message_view.getHeight + message_offset
+    while (y >= 0 && n >= 0){
+      val panel = set_message (n, y)
+      y = y - panel.getHeight
+      n = n - 1
+    }
+    //clean cache (except for some elements on top and bottom, if existent)
+    //TODO: find appropriate values
+    //larger cache makes e.g. resizing slower
+    if(message_cache.size > 20){
+      val min = n - 5
+      val max = message_no + 5
+      message_cache = message_cache filter (t => t match{case (no, _) => no >= min && no <= max})
+    }
+    repaint()
   }
 
-  def add_message (message : T) = {
+  def add_message (message: Document) = {
     message_buffer += message
+    vscroll.setMaximum (Math.max(1, message_buffer.length))
   }
 
   override def adjustmentValueChanged (e : AdjustmentEvent) = {
-    //TODO: find out if all Swing-Implementations handle scrolling as *only* TRACK
-    e.getAdjustmentType match {
-      //Scroll shown messages up
-      case AdjustmentEvent.UNIT_INCREMENT =>
-
-      //Scroll shown messages down
-      case AdjustmentEvent.UNIT_DECREMENT =>
-
-      // Jump to next message
-      case AdjustmentEvent.BLOCK_INCREMENT =>
-
-      //Jump to previous message
-      case AdjustmentEvent.BLOCK_DECREMENT =>
-
-      //Jump to message
-      case AdjustmentEvent.TRACK =>
-        message_no = e.getValue
-        update_view
-      case _ =>
+    //event-handling has to be so general (without UNIT_INCR,...)
+    // because all events could be sent as TRACK e.g. on my mac
+    message_no = e.getValue
+    update_view
+  }
+  
+  override def componentHidden(e: ComponentEvent){}
+  override def componentMoved(e: ComponentEvent){}
+  override def componentResized(e: ComponentEvent){
+    // update_cache: insert panels into new cache -> preferred size is calculated
+    val panels = message_cache.elements
+    message_cache = message_cache.empty
+    panels foreach (pair => pair match{case (no, pa) => add_to_cache (no, pa)})
+    vscroll.setMaximum (Math.max(1, message_buffer.length))    
+    update_view
+  }
+  override def componentShown(e: ComponentEvent){}
+  
+  //register somewhere
+  Plugin.plugin.stateUpdate.add(state => {
+    var i = 0
+    if(state != null) while (i < 500) {
+      add_message(state.document)
+      i += 1
     }
-  }
-  }
+  })
+}
 
 
-class XMLScroller(view : View, position : String) extends LazyScroller[Document] {
-  
-    Plugin.plugin.stateUpdate.add(state => {
-        var i = 0
-        if(state != null) while (i < 1000) {
-          add_message(state.document)
-          i += 1
-        }
-        //TODO: only a hack:
-        update_scrollbar
-    })
-
-    def render (message: Document): JPanel = {
-      val panel = new XHTMLPanel(new UserAgent())
-
-      val fontResolver =
-        panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
-      if (Plugin.plugin.viewFont != null)
-        fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
-
-      Plugin.plugin.viewFontChanged.add(font => {
-        if (Plugin.plugin.viewFont != null)
-          fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
-
-        panel.relayout()
-      })
-
-      panel.setDocument(message, LazyScroller.baseURL)
-      panel
-    }
- }
-