# HG changeset patch
# User immler@in.tum.de
# Date 1224764164 -7200
# Node ID b2781f2cd80a5fb6ad405836920668b23475e153
# Parent 6df5642a2204f4805c850973c631265cfae3bb8d
LazyScroller: rendering messages only when needed
- very basic functionallity
diff -r 6df5642a2204 -r b2781f2cd80a src/Tools/jEdit/plugin/IsabellePlugin.props
--- a/src/Tools/jEdit/plugin/IsabellePlugin.props Wed Oct 22 23:52:40 2008 +0200
+++ b/src/Tools/jEdit/plugin/IsabellePlugin.props Thu Oct 23 14:16:04 2008 +0200
@@ -7,14 +7,16 @@
plugin.isabelle.jedit.Plugin.option-pane=isabelle
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=Isabelle.show-output Isabelle.show-state Isabelle.activate
+plugin.isabelle.jedit.Plugin.menu=Isabelle.show-output Isabelle.show-state Isabelle.activate Isabelle.show-scroller
Isabelle.show-output.label=Show Output
Isabelle.show-state.label=Show State
+Isabelle.show-scroller.label=Show Scroller
Isabelle.activate.label=Activate current buffer
Isabelle_output.title=Isabelle Output
Isabelle_state.title=Isabelle State
+Isabelle_scroller.title=Isabelle Scroller
options.isabelle.label=Isabelle
options.isabelle.code=new isabelle.jedit.OptionPane();
diff -r 6df5642a2204 -r b2781f2cd80a src/Tools/jEdit/plugin/actions.xml
--- a/src/Tools/jEdit/plugin/actions.xml Wed Oct 22 23:52:40 2008 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml Thu Oct 23 14:16:04 2008 +0200
@@ -9,6 +9,11 @@
wm.addDockableWindow("Isabelle_state");
+
+
+ wm.addDockableWindow("Isabelle_scroller");
+
+
isabelle.jedit.Plugin$.MODULE$.plugin().activate(view);
diff -r 6df5642a2204 -r b2781f2cd80a src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml Wed Oct 22 23:52:40 2008 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml Thu Oct 23 14:16:04 2008 +0200
@@ -9,4 +9,7 @@
new isabelle.jedit.StateViewDockable(view, position);
+
+ new isabelle.jedit.XMLScroller(view, position);
+
\ No newline at end of file
diff -r 6df5642a2204 -r b2781f2cd80a src/Tools/jEdit/src/jedit/LazyScroller.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/LazyScroller.scala Thu Oct 23 14:16:04 2008 +0200
@@ -0,0 +1,144 @@
+/*
+ * LazyScroller.scala
+ *
+ *
+ */
+
+package isabelle.jedit
+
+import java.io.{ ByteArrayInputStream, FileInputStream, InputStream }
+
+import scala.collection.mutable.ArrayBuffer
+import scala.collection.jcl.ArrayList
+
+import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar }
+import java.awt.image.BufferedImage
+import java.awt.event.{ AdjustmentListener, AdjustmentEvent }
+import javax.swing.{ JScrollBar, JPanel, JScrollPane, ScrollPaneConstants }
+
+import isabelle.IsabelleSystem.getenv
+
+import org.xml.sax.InputSource;
+
+import org.w3c.dom.Document
+
+import org.xhtmlrenderer.simple.XHTMLPanel
+import org.xhtmlrenderer.context.AWTFontResolver
+import org.xhtmlrenderer.swing.NaiveUserAgent
+import org.xhtmlrenderer.resource.CSSResource
+
+import org.gjt.sp.jedit.View
+
+object LazyScroller {
+ val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
+ val userStylesheet =
+ "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css";
+ val stylesheet = """
+
+@import "isabelle.css";
+
+@import '""" + userStylesheet + """';
+
+messages, message {
+ display: block;
+ white-space: pre-wrap;
+ font-family: Isabelle;
+}
+"""
+}
+
+
+abstract class LazyScroller[T] extends JPanel with AdjustmentListener{
+ //holding the unrendered messages
+ val message_buffer = new ArrayBuffer[T]()
+ // defining the current view
+ val scrollunit = 10 //TODO: not used
+ var message_offset = 0 //TODO: not used; how many pixels of the topmost message are hidden
+ var message_no = 0 //index of the topmost message
+ var message_view = new JPanel
+ message_view.setLayout(new GridLayout(1,1))
+ // setting up view
+ setLayout(new BorderLayout())
+ val pane = new JScrollPane(message_view, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS)
+ val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1)
+ vscroll.addAdjustmentListener(this)
+ add (vscroll, BorderLayout.EAST)
+ add (pane, BorderLayout.CENTER)
+
+
+ // subclasses should implement this
+ def render (message : T) : JPanel
+
+ //TODO: - add more than one message
+ // - render only when necessary
+ def update_view = {
+ message_view.removeAll()
+ message_view.add (render (message_buffer(message_no)))
+ }
+
+ def update_scrollbar = {
+ vscroll.setValue (message_no)
+ vscroll.setMaximum (Math.max(1, message_buffer.length))
+ }
+
+ def add_message (message : T) = {
+ message_buffer += message
+ }
+
+ override def adjustmentValueChanged (e : AdjustmentEvent) = {
+ //TODO: find out if all Swing-Implementations handle scrolling as *only* TRACK
+ e.getAdjustmentType match {
+ //Scroll shown messages up
+ case AdjustmentEvent.UNIT_INCREMENT =>
+
+ //Scroll shown messages down
+ case AdjustmentEvent.UNIT_DECREMENT =>
+
+ // Jump to next message
+ case AdjustmentEvent.BLOCK_INCREMENT =>
+
+ //Jump to previous message
+ case AdjustmentEvent.BLOCK_DECREMENT =>
+
+ //Jump to message
+ case AdjustmentEvent.TRACK =>
+ message_no = e.getValue
+ update_view
+ case _ =>
+ }
+ }
+}
+
+
+class XMLScroller(view : View, position : String) extends LazyScroller[Document] {
+
+ Plugin.plugin.stateUpdate.add(state => {
+ var i = 0
+ if(state != null) while (i < 10000) {
+ add_message(state.document)
+ i += 1
+ }
+ //TODO: only a hack:
+ update_scrollbar
+ })
+
+ def render (message: Document): JPanel = {
+ val panel = new XHTMLPanel(new UserAgent())
+
+ val fontResolver =
+ panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
+ if (Plugin.plugin.viewFont != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+ Plugin.plugin.viewFontChanged.add(font => {
+ if (Plugin.plugin.viewFont != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+ panel.relayout()
+ })
+
+ panel.setDocument(message, LazyScroller.baseURL)
+ panel
+ }
+ }
+