src/Tools/jEdit/src/jedit/ScrollerDockable.scala
author immler@in.tum.de
Tue, 18 Nov 2008 22:07:40 +0100
changeset 34374 b41c1b50e0a9
parent 34371 4a63526bead1
child 34375 71e86ec7e159
permissions -rw-r--r--
buffer as array
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     1
/*
34349
1714aeef8388 renamed class
immler@in.tum.de
parents: 34348
diff changeset
     2
 * ScrollerDockable.scala
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     3
 *
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     4
 */
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     5
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     6
package isabelle.jedit
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
     7
34370
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
     8
import isabelle.utils.EventSource
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
     9
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    10
import scala.collection.mutable.{ArrayBuffer, HashMap}
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    11
34359
e4ca265c9c8b removed imports
immler@in.tum.de
parents: 34358
diff changeset
    12
import java.awt.{ BorderLayout, Adjustable }
34357
61674cd653f9 scroll to first message immediately; potential later messages periodically
immler@in.tum.de
parents: 34356
diff changeset
    13
import java.awt.event.{ ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    14
import javax.swing.{ JFrame, JPanel, JRadioButton, JScrollBar, JTextArea, Timer }
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    15
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    16
import org.w3c.dom.Document
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    17
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    18
import org.xhtmlrenderer.simple.XHTMLPanel
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    19
import org.xhtmlrenderer.context.AWTFontResolver
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    20
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    21
import org.gjt.sp.jedit.View
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    22
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    23
trait Unrendered[T] {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    24
  def addUnrendered (id: Int, u: T) : Unit
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    25
  def getUnrendered (id: Int) : Option[T]
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    26
  def size : Int
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    27
}
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
    28
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    29
trait Rendered[T] {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    30
  def getRendered (id: Int) : Option[T]
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    31
}
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
    32
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    33
object Renderer {
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents: 34370
diff changeset
    34
  
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    35
  def render (message: Document): XHTMLPanel = {
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    36
    val panel = new XHTMLPanel(new UserAgent())
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    37
    val fontResolver =
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    38
      panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    39
    if (Plugin.plugin.viewFont != null)
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    40
      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    41
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    42
    Plugin.plugin.viewFontChanged.add(font => {
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    43
      if (Plugin.plugin.viewFont != null)
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    44
        fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    45
      panel.relayout()
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    46
    })
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    47
    panel.setDocument(message, UserAgent.baseURL)
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents: 34370
diff changeset
    48
    val sa = new SelectionActions
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents: 34370
diff changeset
    49
    sa.install(panel)
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    50
    panel
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    51
  }
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    52
  
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    53
  def relayout_panel (panel: XHTMLPanel, width : Int) {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    54
    // ATTENTION:
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    55
    // panel has to be displayable in a frame/container message_view for doDocumentLayout to have
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    56
    // an effect, especially returning correct preferredSize
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    57
    panel.setBounds (0, 0, width, 1) // document has to fit into width
34361
3e7568e833d9 selecting text of state view
immler@in.tum.de
parents: 34360
diff changeset
    58
    panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then
34358
57a8536d09d3 minimum height for panels, immediate scrolling and correct waiting
immler@in.tum.de
parents: 34357
diff changeset
    59
    // if there are thousands of empty panels, all have to be rendered -
57a8536d09d3 minimum height for panels, immediate scrolling and correct waiting
immler@in.tum.de
parents: 34357
diff changeset
    60
    // but this takes time (even for empty panels); therefore minimum size
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    61
    panel.setPreferredSize(new java.awt.Dimension(width,Math.max(25, panel.getPreferredSize.getHeight.toInt)))
34346
634024f57c18 faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents: 34344
diff changeset
    62
  }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    63
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    64
}
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    65
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    66
class MessagePanel(cache: Rendered[XHTMLPanel]) extends JPanel {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    67
  // defining the current view
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
    68
  var offset = 0 //what percentage of the lowest message is hidden
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    69
  var no = -1  //index of the lowest message
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    70
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    71
  // preferences
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    72
  val scrollunit = 5
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    73
  setLayout(null)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    74
  
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    75
  // place the bottom of the message at y-coordinate and return the rendered panel
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    76
  def place_message (message_no: Int, y: Int) = {
34354
110f5f6902dc cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents: 34353
diff changeset
    77
    //add panel to cache if necessary and possible
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    78
    cache.getRendered(message_no) match {
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    79
      case Some(panel) => {
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    80
        //panel has to be displayable before calculating preferred size!
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    81
        add(panel)
34354
110f5f6902dc cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents: 34353
diff changeset
    82
        // recalculate preferred size after resizing the message_view
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    83
        if(panel.getPreferredSize.getWidth.toInt != getWidth){
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    84
          Renderer.relayout_panel (panel, getWidth)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    85
        }
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    86
        val width = panel.getPreferredSize.getWidth.toInt
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    87
        val height = panel.getPreferredSize.getHeight.toInt
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    88
        panel.setBounds(0, y - height, width, height)
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    89
        panel
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    90
      }
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    91
      case None => null
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents: 34351
diff changeset
    92
    }
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
    93
  }
34351
1c919f65c296 fine scrolling principally possible
immler@in.tum.de
parents: 34350
diff changeset
    94
  
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    95
  override def doLayout = {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
    96
    removeAll()
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
    97
    //calculate offset in pixel
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
    98
    val panel = place_message(no, 0)
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
    99
    val pixeloffset = if(panel != null) panel.getHeight*offset/100 else 0
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   100
    var n = no
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   101
    var y:Int = getHeight + pixeloffset
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   102
    while (y >= 0 && n >= 0){
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   103
      val panel = place_message (n, y)
34370
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   104
      if(panel != null) {
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   105
        panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder)
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   106
        y = y - panel.getHeight
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   107
      }
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   108
      n = n - 1
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   109
    }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   110
  }  
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   111
}
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   112
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   113
class InfoPanel extends JPanel {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   114
  val auto_scroll = new JRadioButton("Auto Scroll", false)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   115
  val message_ind = new JTextArea("0")
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   116
  add(message_ind)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   117
  add(auto_scroll)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   118
  
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   119
  def isAutoScroll = auto_scroll.isSelected
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   120
  def setIndicator(b: Boolean) = {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   121
    message_ind.setBackground(if (b) java.awt.Color.red else java.awt.Color.white)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   122
  }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   123
  def setText(s: String) {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   124
    message_ind.setText(s)
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   125
  }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   126
  
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   127
}
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   128
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   129
class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   130
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   131
  val buffer:Unrendered[Document] = new MessageBuffer()
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   132
  val cache:Rendered[XHTMLPanel] = new PanelCache(buffer)
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   133
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   134
  val subunits = 100
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   135
  // set up view
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   136
  val message_panel = new MessagePanel(cache)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   137
  val infopanel = new InfoPanel
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   138
  val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1)
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   139
  vscroll.setUnitIncrement(subunits / 5)
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   140
  vscroll.setBlockIncrement(subunits / 2)
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   141
  vscroll.addAdjustmentListener(this)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   142
  
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   143
  setLayout(new BorderLayout())
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   144
  add (vscroll, BorderLayout.EAST)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   145
  add (message_panel, BorderLayout.CENTER)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   146
  add (infopanel, BorderLayout.SOUTH)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   147
  
34365
5691af1d34cd renamed to message_panel
immler@in.tum.de
parents: 34361
diff changeset
   148
  // do not show every new message, wait a certain amount of time
5691af1d34cd renamed to message_panel
immler@in.tum.de
parents: 34361
diff changeset
   149
  val message_ind_timer : Timer = new Timer(250, new ActionListener {
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   150
      // this method is called to indicate a new message
34357
61674cd653f9 scroll to first message immediately; potential later messages periodically
immler@in.tum.de
parents: 34356
diff changeset
   151
      override def actionPerformed(e:ActionEvent){
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   152
        //fire scroll-event if necessary and wanted
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   153
        if(message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   154
          vscroll.setValue(buffer.size*subunits - 1)
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   155
        }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   156
        infopanel.setIndicator(false)
34357
61674cd653f9 scroll to first message immediately; potential later messages periodically
immler@in.tum.de
parents: 34356
diff changeset
   157
      }
61674cd653f9 scroll to first message immediately; potential later messages periodically
immler@in.tum.de
parents: 34356
diff changeset
   158
    })
61674cd653f9 scroll to first message immediately; potential later messages periodically
immler@in.tum.de
parents: 34356
diff changeset
   159
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   160
  def add_message (message: Document) = {
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   161
    buffer.addUnrendered(buffer.size, message)
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   162
    vscroll.setMaximum (Math.max(1, buffer.size * subunits))
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   163
    infopanel.setIndicator(true)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   164
    infopanel.setText(buffer.size.toString)
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   165
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   166
    if (! message_ind_timer.isRunning()){
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   167
      if(infopanel.isAutoScroll){
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   168
        vscroll.setValue(buffer.size*subunits - 1)
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   169
      }
34360
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   170
      message_ind_timer.setRepeats(false)
b7af69a030a1 worked over autoscrolling
immler@in.tum.de
parents: 34359
diff changeset
   171
      message_ind_timer.start()
34351
1c919f65c296 fine scrolling principally possible
immler@in.tum.de
parents: 34350
diff changeset
   172
    }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   173
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   174
    if(message_panel.no == -1) {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   175
      message_panel.no = 0
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   176
      message_panel.invalidate
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   177
    }
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   178
  }
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   179
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   180
  override def adjustmentValueChanged (e : AdjustmentEvent) = {
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   181
    //event-handling has to be so general (without UNIT_INCR,...)
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   182
    // because all events could be sent as TRACK e.g. on my mac
34355
3ae10f5d40aa prepared for automatic scrolling
immler@in.tum.de
parents: 34354
diff changeset
   183
    if (e.getSource == vscroll){
34368
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   184
      message_panel.no = e.getValue / subunits
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   185
      message_panel.offset = 100 - 100 * (e.getValue % subunits) / subunits
8ba358ac69a8 fine grained scrolling
immler@in.tum.de
parents: 34367
diff changeset
   186
      message_panel.invalidate
34355
3ae10f5d40aa prepared for automatic scrolling
immler@in.tum.de
parents: 34354
diff changeset
   187
    }
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   188
  }
34346
634024f57c18 faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents: 34344
diff changeset
   189
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   190
  
34370
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   191
  // TODO: register
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34369
diff changeset
   192
  Plugin.plugin.prover.allInfo.add(add_message(_))
34344
3775958051c5 absolute positioning according to preferred size of panels,
immler@in.tum.de
parents: 34343
diff changeset
   193
}
34342
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   194
b2781f2cd80a LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff changeset
   195
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   196
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   197
//containing the unrendered messages
34374
b41c1b50e0a9 buffer as array
immler@in.tum.de
parents: 34371
diff changeset
   198
class MessageBuffer extends ArrayBuffer[Document] with Unrendered[Document]{
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   199
  override def addUnrendered (id: Int, m: Document) {
34374
b41c1b50e0a9 buffer as array
immler@in.tum.de
parents: 34371
diff changeset
   200
    append(m)
34366
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   201
  }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   202
  override def getUnrendered (id: Int): Option[Document] = {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   203
    if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   204
    else None
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   205
  }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   206
  override def size = super.size
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   207
}
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   208
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   209
//containing the rendered messages
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   210
class PanelCache (buffer: Unrendered[Document]) extends HashMap[Int, XHTMLPanel] with Rendered[XHTMLPanel]{
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   211
  override def getRendered (id: Int): Option[XHTMLPanel] = {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   212
    //get message from buffer and render it if necessary
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   213
    if(!isDefinedAt(id)){
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   214
      buffer.getUnrendered(id) match {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   215
        case Some (message) =>
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   216
          update (id, Renderer.render (message))
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   217
        case None =>
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   218
      }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   219
    }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   220
    val result = try {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   221
      Some (apply(id))
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   222
    } catch {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   223
      case _ => {
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   224
          None
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   225
      }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   226
    }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   227
    return result
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   228
  }
2f6e50fa7ac4 restructured scroller
immler@in.tum.de
parents: 34365
diff changeset
   229
}