# HG changeset patch # User immler@in.tum.de # Date 1227012198 -3600 # Node ID 2f6e50fa7ac45868624e63a338ce560423ff045c # Parent 5691af1d34cd462531eb9b3adbae94ed9bc737ff restructured scroller diff -r 5691af1d34cd -r 2f6e50fa7ac4 src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Nov 17 16:39:39 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Tue Nov 18 13:43:18 2008 +0100 @@ -1,18 +1,17 @@ /* * ScrollerDockable.scala * - * TODO: clearer seperation of tasks: layout message_view, layout panel (with preferredsize), repaint, relayout, ... - * + relayout on ValueIsAdjusting while scrolling + * TODO: * + scrolling *one* panel */ package isabelle.jedit -import scala.collection.mutable.ArrayBuffer +import scala.collection.mutable.{ArrayBuffer, HashMap} import java.awt.{ BorderLayout, Adjustable } import java.awt.event.{ ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent } -import javax.swing.{ JPanel, JRadioButton, JScrollBar, JTextArea, Timer } +import javax.swing.{ JFrame, JPanel, JRadioButton, JScrollBar, JTextArea, Timer } import org.w3c.dom.Document @@ -21,39 +20,17 @@ import org.gjt.sp.jedit.View -class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener { - //holding the unrendered messages - val message_buffer = new ArrayBuffer[Document]() - //rendered messages - var message_cache = Map[Int, XHTMLPanel]() - // defining the current view - val scrollunit = 1 - 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_panel = new JPanel - message_panel.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_panel, BorderLayout.CENTER) - addComponentListener(this) - //automated scrolling, new message ind - val infopanel = new JPanel - val auto_scroll = new JRadioButton("Auto Scroll", false) - //indicates new messages with a new color, and shows number of messages in cache - val message_ind = new JTextArea("0") - infopanel.add(message_ind) - infopanel.add(auto_scroll) - add (infopanel, BorderLayout.SOUTH) +trait Unrendered[T] { + def addUnrendered (id: Int, u: T) : Unit + def getUnrendered (id: Int) : Option[T] + def size : Int +} - // DoubleBuffering for smoother updates - this.setDoubleBuffered(true) - message_panel.setDoubleBuffered(true) +trait Rendered[T] { + def getRendered (id: Int) : Option[T] +} - //Render a message to a Panel +object Renderer { def render (message: Document): XHTMLPanel = { val panel = new XHTMLPanel(new UserAgent()) val fontResolver = @@ -64,46 +41,52 @@ Plugin.plugin.viewFontChanged.add(font => { if (Plugin.plugin.viewFont != null) fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) - panel.relayout() }) - panel.setDocument(message, UserAgent.baseURL) panel } - // panel has to be displayable in container message_view for doLayout to have - // an effect, especially returning correct preferredSize - def calculate_preferred_size(panel: XHTMLPanel){ - message_panel.add (panel) - panel.setBounds (0, 0, message_panel.getWidth, 1) // document has to fit into width + def relayout_panel (panel: XHTMLPanel, width : Int) { + // ATTENTION: + // panel has to be displayable in a frame/container message_view for doDocumentLayout to have + // an effect, especially returning correct preferredSize + panel.setBounds (0, 0, width, 1) // document has to fit into width panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then // if there are thousands of empty panels, all have to be rendered - // but this takes time (even for empty panels); therefore minimum size - panel.setPreferredSize(new java.awt.Dimension(message_panel.getWidth,Math.max(50, panel.getPreferredSize.getHeight.toInt))) + panel.setPreferredSize(new java.awt.Dimension(width,Math.max(25, panel.getPreferredSize.getHeight.toInt))) } - - //render and load a message into cache, place its bottom at y-coordinate; - def set_message (message_no: Int, y: Int) = { + +} + +class MessagePanel(cache: Rendered[XHTMLPanel]) extends JPanel { + // defining the current view + var offset = 0 //how many pixels of the lowest message are hidden + var no = -1 //index of the lowest message + + // preferences + val scrollunit = 5 + setLayout(null) + + // place the bottom of the message at y-coordinate and return the rendered panel + def place_message (message_no: Int, y: Int) = { //add panel to cache if necessary and possible - if(!message_cache.isDefinedAt(message_no) && message_buffer.isDefinedAt(message_no)){ - message_cache = message_cache.update (message_no, render (message_buffer(message_no))) - } - val result = message_cache.get(message_no) match { + cache.getRendered(message_no) match { case Some(panel) => { + //panel has to be displayable before calculating preferred size! + add(panel) // recalculate preferred size after resizing the message_view - if(panel.getPreferredSize.getWidth.toInt != message_panel.getWidth) - calculate_preferred_size (panel) - //place message on view + if(panel.getPreferredSize.getWidth.toInt != getWidth){ + Renderer.relayout_panel (panel, getWidth) + } val width = panel.getPreferredSize.getWidth.toInt val height = panel.getPreferredSize.getHeight.toInt panel.setBounds(0, y - height, width, height) - message_panel.add(panel) panel } case None => null } - result } //move view a given amount of pixels @@ -111,98 +94,135 @@ // (no knowledge on height of messages) def move_view (y : Int) = { var update = false - if(message_panel.getComponentCount >= 1){ - message_offset += y + if(getComponentCount >= 1){ + offset += y //remove bottommost panels - while (message_offset >= message_panel.getComponent(0).getHeight) + while (offset >= getComponent(0).getHeight) { - message_offset -= message_panel.getComponent(0).getHeight - message_no -= 1 - update_view + offset -= getComponent(0).getHeight + no -= 1 + invalidate update = true } //insert panels at the bottom - while (message_offset < 0) { - message_no += 1 - val panel = set_message (message_no, 0) - message_offset += panel.getHeight - update_view + while (offset < 0) { + no += 1 + val panel = place_message (no, 0) + offset += panel.getHeight + invalidate update = true } //insert panel at the top - if (message_panel.getComponent(message_panel.getComponentCount - 1).getY + y > 0){ - update_view + if (getComponent(getComponentCount - 1).getY + y > 0){ + invalidate update = true } //simply move panels if(!update){ - message_panel.getComponents map (c => { + getComponents map (c => { val newrect = c.getBounds newrect.y = newrect.y + y c.setBounds(newrect) }) repaint() } else { - vscroll.setValue(message_no) + //vscroll.setValue(no) + //TODO: create method to update vscroll + System.err.println("lookatme2") } } } - def update_view = { - message_panel.removeAll() - var n = message_no - var y:Int = message_panel.getHeight + message_offset + override def doLayout = { + removeAll() + var n = no + var y:Int = getHeight + offset while (y >= 0 && n >= 0){ - val panel = set_message (n, y) + val panel = place_message (n, y) panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder) y = y - panel.getHeight n = n - 1 } - repaint() + } +} + +class InfoPanel extends JPanel { + val auto_scroll = new JRadioButton("Auto Scroll", false) + val message_ind = new JTextArea("0") + add(message_ind) + add(auto_scroll) + + def isAutoScroll = auto_scroll.isSelected + def setIndicator(b: Boolean) = { + message_ind.setBackground(if (b) java.awt.Color.red else java.awt.Color.white) + } + def setText(s: String) { + message_ind.setText(s) } + +} +class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener { + + val buffer:Unrendered[Document] = new MessageBuffer() + val cache:Rendered[XHTMLPanel] = new PanelCache(buffer) + + // set up view + val message_panel = new MessagePanel(cache) + val infopanel = new InfoPanel + val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1) + vscroll.addAdjustmentListener(this) + + setLayout(new BorderLayout()) + add (vscroll, BorderLayout.EAST) + add (message_panel, BorderLayout.CENTER) + add (infopanel, BorderLayout.SOUTH) + // do not show every new message, wait a certain amount of time val message_ind_timer : Timer = new Timer(250, new ActionListener { // this method is called to indicate a new message override def actionPerformed(e:ActionEvent){ //fire scroll-event if necessary and wanted - if(message_no != message_buffer.size - && auto_scroll.isSelected) { - vscroll.setValue(message_buffer.size - 1) + if(message_panel.no != buffer.size && infopanel.isAutoScroll) { + vscroll.setValue(buffer.size - 1) } - message_ind.setBackground(java.awt.Color.white) + infopanel.setIndicator(false) } }) def add_message (message: Document) = { - message_buffer += message - vscroll.setMaximum (Math.max(1, message_buffer.size)) - message_ind.setBackground(java.awt.Color.red) - message_ind.setText(message_buffer.size.toString) + buffer.addUnrendered(buffer.size, message) + vscroll.setMaximum (Math.max(1, buffer.size)) + infopanel.setIndicator(true) + infopanel.setText(buffer.size.toString) + if (! message_ind_timer.isRunning()){ - if(auto_scroll.isSelected) vscroll.setValue(message_buffer.size - 1) + if(infopanel.isAutoScroll){ + vscroll.setValue(buffer.size - 1) + } message_ind_timer.setRepeats(false) message_ind_timer.start() } + + if(message_panel.no == -1) { + message_panel.no = 0 + message_panel.invalidate + } } - + override def adjustmentValueChanged (e : AdjustmentEvent) = { //event-handling has to be so general (without UNIT_INCR,...) // because all events could be sent as TRACK e.g. on my mac if (e.getSource == vscroll){ - message_no = e.getValue - message_offset = 0 - update_view + message_panel.no = e.getValue + message_panel.offset = 0 + message_panel.invalidate + System.err.println("event: "+message_panel.no) + vscroll.setModel(new javax.swing.DefaultBoundedRangeModel(99,1,0,1000)) + System.err.println("hello"+e.getValue) } } - // handle Component-Events - override def componentShown(e: ComponentEvent){} - override def componentHidden(e: ComponentEvent){} - override def componentMoved(e: ComponentEvent){} - override def componentResized(e: ComponentEvent){ - update_view - } // TODO: register somewhere // here only 'emulation of message stream' @@ -210,7 +230,7 @@ var i = 0 if(state != null) new Thread{ override def run() { - while (i < 500) { + while (i < 1) { add_message(state.document) i += 1 try {Thread.sleep(3)} @@ -222,3 +242,37 @@ } + +//containing the unrendered messages +class MessageBuffer extends HashMap[Int,Document] with Unrendered[Document]{ + override def addUnrendered (id: Int, m: Document) { + update(id, m) + } + override def getUnrendered (id: Int): Option[Document] = { + if(id < size && id >= 0 && apply(id) != null) Some (apply(id)) + else None + } + override def size = super.size +} + +//containing the rendered messages +class PanelCache (buffer: Unrendered[Document]) extends HashMap[Int, XHTMLPanel] with Rendered[XHTMLPanel]{ + override def getRendered (id: Int): Option[XHTMLPanel] = { + //get message from buffer and render it if necessary + if(!isDefinedAt(id)){ + buffer.getUnrendered(id) match { + case Some (message) => + update (id, Renderer.render (message)) + case None => + } + } + val result = try { + Some (apply(id)) + } catch { + case _ => { + None + } + } + return result + } +} \ No newline at end of file