--- 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