author | immler@in.tum.de |
Sun, 26 Oct 2008 00:10:39 +0200 | |
changeset 34343 | 4a3bdb561d11 |
parent 34342 | b2781f2cd80a |
child 34344 | 3775958051c5 |
permissions | -rw-r--r-- |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
1 |
/* |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
2 |
* LazyScroller.scala |
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 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
7 |
package isabelle.jedit |
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 |
import java.io.{ ByteArrayInputStream, FileInputStream, InputStream } |
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 scala.collection.mutable.ArrayBuffer |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
12 |
import scala.collection.jcl.ArrayList |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
13 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
14 |
import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar } |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
15 |
import java.awt.image.BufferedImage |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
16 |
import java.awt.event.{ AdjustmentListener, AdjustmentEvent } |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
17 |
import javax.swing.{ JScrollBar, JPanel, JScrollPane, ScrollPaneConstants } |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
18 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
19 |
import isabelle.IsabelleSystem.getenv |
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.xml.sax.InputSource; |
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.w3c.dom.Document |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
24 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
25 |
import org.xhtmlrenderer.simple.XHTMLPanel |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
26 |
import org.xhtmlrenderer.context.AWTFontResolver |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
27 |
import org.xhtmlrenderer.swing.NaiveUserAgent |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
28 |
import org.xhtmlrenderer.resource.CSSResource |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
29 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
30 |
import org.gjt.sp.jedit.View |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
31 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
32 |
object LazyScroller { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
33 |
val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/" |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
34 |
val userStylesheet = |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
35 |
"file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
36 |
val stylesheet = """ |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
37 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
38 |
@import "isabelle.css"; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
39 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
40 |
@import '""" + userStylesheet + """'; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
41 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
42 |
messages, message { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
43 |
display: block; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
44 |
white-space: pre-wrap; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
45 |
font-family: Isabelle; |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
46 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
47 |
""" |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
48 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
49 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
50 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
51 |
abstract class LazyScroller[T] extends JPanel with AdjustmentListener{ |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
52 |
//holding the unrendered messages |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
53 |
val message_buffer = new ArrayBuffer[T]() |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
54 |
// defining the current view |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
55 |
val scrollunit = 10 //TODO: not used |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
56 |
var message_offset = 0 //TODO: not used; how many pixels of the topmost message are hidden |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
57 |
var message_no = 0 //index of the topmost message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
58 |
var message_view = new JPanel |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
59 |
message_view.setLayout(new GridLayout(1,1)) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
60 |
// setting up view |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
61 |
setLayout(new BorderLayout()) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
62 |
val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
63 |
vscroll.addAdjustmentListener(this) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
64 |
add (vscroll, BorderLayout.EAST) |
34343 | 65 |
add (message_view, BorderLayout.CENTER) |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
66 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
67 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
68 |
// subclasses should implement this |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
69 |
def render (message : T) : JPanel |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
70 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
71 |
//TODO: - add more than one message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
72 |
// - render only when necessary |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
73 |
def update_view = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
74 |
message_view.removeAll() |
34343 | 75 |
val rendered_message = render (message_buffer(message_no)) |
76 |
val resizable = new JScrollPane(rendered_message, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER) |
|
77 |
message_view.add (resizable) |
|
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
78 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
79 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
80 |
def update_scrollbar = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
81 |
vscroll.setValue (message_no) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
82 |
vscroll.setMaximum (Math.max(1, message_buffer.length)) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
83 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
84 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
85 |
def add_message (message : T) = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
86 |
message_buffer += message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
87 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
88 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
89 |
override def adjustmentValueChanged (e : AdjustmentEvent) = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
90 |
//TODO: find out if all Swing-Implementations handle scrolling as *only* TRACK |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
91 |
e.getAdjustmentType match { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
92 |
//Scroll shown messages up |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
93 |
case AdjustmentEvent.UNIT_INCREMENT => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
94 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
95 |
//Scroll shown messages down |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
96 |
case AdjustmentEvent.UNIT_DECREMENT => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
97 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
98 |
// Jump to next message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
99 |
case AdjustmentEvent.BLOCK_INCREMENT => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
100 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
101 |
//Jump to previous message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
102 |
case AdjustmentEvent.BLOCK_DECREMENT => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
103 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
104 |
//Jump to message |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
105 |
case AdjustmentEvent.TRACK => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
106 |
message_no = e.getValue |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
107 |
update_view |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
108 |
case _ => |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
109 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
110 |
} |
34343 | 111 |
} |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
112 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
113 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
114 |
class XMLScroller(view : View, position : String) extends LazyScroller[Document] { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
115 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
116 |
Plugin.plugin.stateUpdate.add(state => { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
117 |
var i = 0 |
34343 | 118 |
if(state != null) while (i < 1000) { |
34342
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
119 |
add_message(state.document) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
120 |
i += 1 |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
121 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
122 |
//TODO: only a hack: |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
123 |
update_scrollbar |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
124 |
}) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
125 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
126 |
def render (message: Document): JPanel = { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
127 |
val panel = new XHTMLPanel(new UserAgent()) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
128 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
129 |
val fontResolver = |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
130 |
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
131 |
if (Plugin.plugin.viewFont != null) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
132 |
fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
133 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
134 |
Plugin.plugin.viewFontChanged.add(font => { |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
135 |
if (Plugin.plugin.viewFont != null) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
136 |
fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
137 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
138 |
panel.relayout() |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
139 |
}) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
140 |
|
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
141 |
panel.setDocument(message, LazyScroller.baseURL) |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
142 |
panel |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
143 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
144 |
} |
b2781f2cd80a
LazyScroller: rendering messages only when needed
immler@in.tum.de
parents:
diff
changeset
|
145 |