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