author | immler@in.tum.de |
Mon, 03 Nov 2008 18:44:48 +0100 | |
changeset 34355 | 3ae10f5d40aa |
parent 34354 | 110f5f6902dc |
child 34356 | 3d6f4dd10e63 |
permissions | -rw-r--r-- |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
1 |
/* |
34349 | 2 |
* ScrollerDockable.scala |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
3 |
* |
34346
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
4 |
* TODO: clearer seperation of tasks: layout message_view, layout panel (with preferredsize), repaint, relayout, ... |
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
5 |
* + relayout on ValueIsAdjusting while scrolling |
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
6 |
* + scrolling *one* panel |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
7 |
*/ |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
8 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
9 |
package isabelle.jedit |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
10 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
11 |
import java.io.{ ByteArrayInputStream, FileInputStream, InputStream } |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
12 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
13 |
import scala.collection.mutable.ArrayBuffer |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
14 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
15 |
import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar } |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
16 |
import java.awt.image.BufferedImage |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
17 |
import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent } |
34355 | 18 |
import javax.swing.{ JPanel, JRadioButton, JScrollBar, JScrollPane, JTextArea, ScrollPaneConstants } |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
19 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
20 |
import isabelle.IsabelleSystem.getenv |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
21 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
22 |
import org.xml.sax.InputSource; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
23 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
24 |
import org.w3c.dom.Document |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
25 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
26 |
import org.xhtmlrenderer.simple.XHTMLPanel |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
27 |
import org.xhtmlrenderer.context.AWTFontResolver |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
28 |
import org.xhtmlrenderer.swing.NaiveUserAgent |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
29 |
import org.xhtmlrenderer.resource.CSSResource |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
30 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
31 |
import org.gjt.sp.jedit.View |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
32 |
|
34349 | 33 |
class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener { |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
34 |
//holding the unrendered messages |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
35 |
val message_buffer = new ArrayBuffer[Document]() |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
36 |
//rendered messages |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
37 |
var message_cache = Map[Int, XHTMLPanel]() |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
38 |
// defining the current view |
34355 | 39 |
val scrollunit = 1 |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
40 |
var message_offset = 0 //how many pixels of the lowest message are hidden |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
41 |
var message_no = -1 //index of the lowest message |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
42 |
// absolute positioning for messages |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
43 |
val message_view = new JPanel |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
44 |
message_view.setLayout(null) |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
45 |
// setting up view |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
46 |
setLayout(new BorderLayout()) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
47 |
val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
48 |
vscroll.addAdjustmentListener(this) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
49 |
add (vscroll, BorderLayout.EAST) |
34343 | 50 |
add (message_view, BorderLayout.CENTER) |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
51 |
addComponentListener(this) |
34355 | 52 |
//automated scrolling, new message ind |
53 |
val infopanel = new JPanel |
|
54 |
val auto_scroll = new JRadioButton("Auto Scroll", false) |
|
55 |
val new_message_ind = new JTextArea("0") |
|
56 |
infopanel.add(new_message_ind) |
|
57 |
infopanel.add(auto_scroll) |
|
58 |
add (infopanel, BorderLayout.SOUTH) |
|
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
59 |
|
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
60 |
//Render a message to a Panel |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
61 |
def render (message: Document): XHTMLPanel = { |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
62 |
val panel = new XHTMLPanel(new UserAgent()) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
63 |
|
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
64 |
val fontResolver = |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
65 |
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
66 |
if (Plugin.plugin.viewFont != null) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
67 |
fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
68 |
|
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
69 |
Plugin.plugin.viewFontChanged.add(font => { |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
70 |
if (Plugin.plugin.viewFont != null) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
71 |
fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
72 |
|
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
73 |
panel.relayout() |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
74 |
}) |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
75 |
|
34353
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
76 |
panel.setDocument(message, UserAgent.baseURL) |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
77 |
panel |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
78 |
} |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
79 |
|
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
80 |
// panel has to be displayable in container message_view for doLayout to have |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
81 |
// an effect, especially returning correct preferredSize |
34346
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
82 |
def calculate_preferred_size(panel: XHTMLPanel){ |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
83 |
message_view.add (panel) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
84 |
panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
85 |
panel.doLayout (panel.getGraphics) //lay out, preferred size is set then |
34346
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
86 |
} |
34351 | 87 |
|
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
88 |
//render and load a message into cache, place its bottom at y-coordinate; |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
89 |
def set_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
|
90 |
//add panel to cache if necessary and possible |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
91 |
if(!message_cache.isDefinedAt(message_no) && message_buffer.isDefinedAt(message_no)){ |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
92 |
message_cache = message_cache.update (message_no, render (message_buffer(message_no))) |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
93 |
} |
34353
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
94 |
val result = message_cache.get(message_no) match { |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
95 |
case Some(panel) => { |
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
96 |
// recalculate preferred size after resizing the message_view |
34353
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
97 |
if(panel.getPreferredSize.getWidth.toInt != message_view.getWidth) |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
98 |
calculate_preferred_size (panel) |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
99 |
//place message on view |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
100 |
val width = panel.getPreferredSize.getWidth.toInt |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
101 |
val height = panel.getPreferredSize.getHeight.toInt |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
102 |
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
|
103 |
message_view.add(panel) |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
104 |
panel |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
105 |
} |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
106 |
case None => null |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
107 |
} |
aa0d2f0bde83
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
34351
diff
changeset
|
108 |
result |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
109 |
} |
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
110 |
|
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
111 |
//move view a given amount of pixels |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
112 |
// attention: y should be small, because messages are rendered incremental |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
113 |
// (no knowledge on height of messages) |
34351 | 114 |
def move_view (y : Int) = { |
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
115 |
var update = false |
34351 | 116 |
if(message_view.getComponentCount >= 1){ |
117 |
message_offset += y |
|
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
118 |
//remove bottommost panels |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
119 |
while (message_offset >= message_view.getComponent(0).getHeight) |
34351 | 120 |
{ |
121 |
message_offset -= message_view.getComponent(0).getHeight |
|
122 |
message_no -= 1 |
|
123 |
update_view |
|
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
124 |
update = true |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
125 |
} |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
126 |
//insert panels at the bottom |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
127 |
while (message_offset < 0) { |
34351 | 128 |
message_no += 1 |
129 |
val panel = set_message (message_no, 0) |
|
130 |
message_offset += panel.getHeight |
|
131 |
update_view |
|
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
132 |
update = true |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
133 |
} |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
134 |
//insert panel at the top |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
135 |
if (message_view.getComponent(message_view.getComponentCount - 1).getY + y > 0){ |
34351 | 136 |
update_view |
34354
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
137 |
update = true |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
138 |
} |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
139 |
//simply move panels |
110f5f6902dc
cleaned up a bit, scrolling arbitrary heights (incremental rendering)
immler@in.tum.de
parents:
34353
diff
changeset
|
140 |
if(!update){ |
34351 | 141 |
message_view.getComponents map (c => { |
142 |
val newrect = c.getBounds |
|
143 |
newrect.y = newrect.y + y |
|
144 |
c.setBounds(newrect) |
|
145 |
}) |
|
146 |
repaint() |
|
34355 | 147 |
} else { |
148 |
vscroll.setValue(message_no) |
|
34351 | 149 |
} |
150 |
} |
|
151 |
} |
|
152 |
||
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
153 |
def update_view = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
154 |
message_view.removeAll() |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
155 |
var n = message_no |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
156 |
var y:Int = message_view.getHeight + message_offset |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
157 |
while (y >= 0 && n >= 0){ |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
158 |
val panel = set_message (n, y) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
159 |
y = y - panel.getHeight |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
160 |
n = n - 1 |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
161 |
} |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
162 |
repaint() |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
163 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
164 |
|
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
165 |
def add_message (message: Document) = { |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
166 |
message_buffer += message |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
167 |
vscroll.setMaximum (Math.max(1, message_buffer.length)) |
34351 | 168 |
if(message_no == -1){ |
169 |
message_no = 0 |
|
170 |
update_view |
|
171 |
} |
|
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
172 |
} |
34351 | 173 |
|
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
174 |
override def adjustmentValueChanged (e : AdjustmentEvent) = { |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
175 |
//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
|
176 |
// because all events could be sent as TRACK e.g. on my mac |
34355 | 177 |
if (e.getSource == vscroll){ |
178 |
message_no = e.getValue |
|
179 |
message_offset = 0 |
|
180 |
update_view |
|
181 |
} |
|
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
182 |
} |
34346
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
183 |
|
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
184 |
// handle Component-Events |
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
185 |
override def componentShown(e: ComponentEvent){} |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
186 |
override def componentHidden(e: ComponentEvent){} |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
187 |
override def componentMoved(e: ComponentEvent){} |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
188 |
override def componentResized(e: ComponentEvent){ |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
189 |
update_view |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
190 |
} |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
191 |
|
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
192 |
//register somewhere |
34346
634024f57c18
faster resizing, unlimited caching(but cache is cleared on resize)
immler@in.tum.de
parents:
34344
diff
changeset
|
193 |
// TODO: only testing atm |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
194 |
Plugin.plugin.stateUpdate.add(state => { |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
195 |
var i = 0 |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
196 |
if(state != null) while (i < 500) { |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
197 |
add_message(state.document) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
198 |
i += 1 |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
199 |
} |
34344
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
200 |
}) |
3775958051c5
absolute positioning according to preferred size of panels,
immler@in.tum.de
parents:
34343
diff
changeset
|
201 |
} |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
202 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
203 |