# HG changeset patch # User immler@in.tum.de # Date 1225632678 -3600 # Node ID abea94120f4b9cc570647b394020154a413bf7cc # Parent 0638419a3cd86f39c90100d9eb3fb88b224da722 renamed diff -r 0638419a3cd8 -r abea94120f4b src/Tools/jEdit/src/jedit/LazyScroller.scala --- a/src/Tools/jEdit/src/jedit/LazyScroller.scala Fri Oct 31 14:50:38 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,172 +0,0 @@ -/* - * LazyScroller.scala - * - * TODO: clearer seperation of tasks: layout message_view, layout panel (with preferredsize), repaint, relayout, ... - * + relayout on ValueIsAdjusting while scrolling - * + scrolling *one* panel - */ - -package isabelle.jedit - -import java.io.{ ByteArrayInputStream, FileInputStream, InputStream } - -import scala.collection.mutable.ArrayBuffer - -import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar } -import java.awt.image.BufferedImage -import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent } -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; -} -""" -} - - -class LazyScroller(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener { - //holding the unrendered messages - val message_buffer = new ArrayBuffer[Document]() - //rendered messages - var message_cache = Map[Int, XHTMLPanel]() - // defining the current view - val scrollunit = 10 - var message_offset = 0 //how many pixels of the lowest message are hidden - var message_no = -1 //index of the lowest message - // absolute positioning for messages - val message_view = new JPanel - message_view.setLayout(null) - // setting up view - setLayout(new BorderLayout()) - val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1) - vscroll.addAdjustmentListener(this) - add (vscroll, BorderLayout.EAST) - add (message_view, BorderLayout.CENTER) - addComponentListener(this) - - - //Render a message to a Panel - def render (message: Document): XHTMLPanel = { - 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 - } - - //calculates preferred size of panel - def calculate_preferred_size(panel: XHTMLPanel){ - message_view.add (panel) - panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width - panel.doLayout (panel.getGraphics) //lay out, preferred size is set then - } - - //add panel to the cache - def add_to_cache (message_no: Int, panel: XHTMLPanel) = { - message_cache = message_cache.update (message_no, panel) - calculate_preferred_size(panel) - System.err.println("Added " + message_no + " with preferred Size " + panel.getPreferredSize + " to cache") - } - - //render and load a message into cache, place its bottom at y-coordinate; - def set_message (message_no: Int, y: Int) = { - //get or add panel from/to cache - if(!message_cache.isDefinedAt(message_no)){ - add_to_cache (message_no, render (message_buffer(message_no))) - } - val panel = message_cache.get(message_no).get - val width = panel.getPreferredSize.getWidth.toInt - val height = panel.getPreferredSize.getHeight.toInt - panel.setBounds(0, y - height, width, height) - message_view.add(panel) - panel - } - - def update_view = { - message_view.removeAll() - var n = message_no - var y:Int = message_view.getHeight + message_offset - while (y >= 0 && n >= 0){ - val panel = set_message (n, y) - y = y - panel.getHeight - n = n - 1 - } - repaint() - } - - def add_message (message: Document) = { - message_buffer += message - vscroll.setMaximum (Math.max(1, message_buffer.length)) - } - - override def adjustmentValueChanged (e : AdjustmentEvent) = { - //event-handling has to be so general (without UNIT_INCR,...) - // because all events could be sent as TRACK e.g. on my mac - message_no = e.getValue - update_view - } - - // handle Component-Events - override def componentShown(e: ComponentEvent){} - override def componentHidden(e: ComponentEvent){} - override def componentMoved(e: ComponentEvent){} - override def componentResized(e: ComponentEvent){ - // remove all hidden messages from cache - // TODO: move to unlayouted cache - message_cache = message_cache filter ( pair => pair match {case (no, _) => - no <= message_no && no >= message_no - message_view.getComponents.length}) - //calculate preferred size for each panel - message_cache foreach (pair => pair match { case (_, pa) => - calculate_preferred_size (pa) - }) - update_view - } - - //register somewhere - // TODO: only testing atm - Plugin.plugin.stateUpdate.add(state => { - var i = 0 - if(state != null) while (i < 500) { - add_message(state.document) - i += 1 - } - }) -} - - diff -r 0638419a3cd8 -r abea94120f4b src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sun Nov 02 14:31:18 2008 +0100 @@ -0,0 +1,172 @@ +/* + * LazyScroller.scala + * + * TODO: clearer seperation of tasks: layout message_view, layout panel (with preferredsize), repaint, relayout, ... + * + relayout on ValueIsAdjusting while scrolling + * + scrolling *one* panel + */ + +package isabelle.jedit + +import java.io.{ ByteArrayInputStream, FileInputStream, InputStream } + +import scala.collection.mutable.ArrayBuffer + +import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar } +import java.awt.image.BufferedImage +import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent } +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; +} +""" +} + + +class LazyScroller(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener { + //holding the unrendered messages + val message_buffer = new ArrayBuffer[Document]() + //rendered messages + var message_cache = Map[Int, XHTMLPanel]() + // defining the current view + val scrollunit = 10 + var message_offset = 0 //how many pixels of the lowest message are hidden + var message_no = -1 //index of the lowest message + // absolute positioning for messages + val message_view = new JPanel + message_view.setLayout(null) + // setting up view + setLayout(new BorderLayout()) + val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1) + vscroll.addAdjustmentListener(this) + add (vscroll, BorderLayout.EAST) + add (message_view, BorderLayout.CENTER) + addComponentListener(this) + + + //Render a message to a Panel + def render (message: Document): XHTMLPanel = { + 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 + } + + //calculates preferred size of panel + def calculate_preferred_size(panel: XHTMLPanel){ + message_view.add (panel) + panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width + panel.doLayout (panel.getGraphics) //lay out, preferred size is set then + } + + //add panel to the cache + def add_to_cache (message_no: Int, panel: XHTMLPanel) = { + message_cache = message_cache.update (message_no, panel) + calculate_preferred_size(panel) + System.err.println("Added " + message_no + " with preferred Size " + panel.getPreferredSize + " to cache") + } + + //render and load a message into cache, place its bottom at y-coordinate; + def set_message (message_no: Int, y: Int) = { + //get or add panel from/to cache + if(!message_cache.isDefinedAt(message_no)){ + add_to_cache (message_no, render (message_buffer(message_no))) + } + val panel = message_cache.get(message_no).get + val width = panel.getPreferredSize.getWidth.toInt + val height = panel.getPreferredSize.getHeight.toInt + panel.setBounds(0, y - height, width, height) + message_view.add(panel) + panel + } + + def update_view = { + message_view.removeAll() + var n = message_no + var y:Int = message_view.getHeight + message_offset + while (y >= 0 && n >= 0){ + val panel = set_message (n, y) + y = y - panel.getHeight + n = n - 1 + } + repaint() + } + + def add_message (message: Document) = { + message_buffer += message + vscroll.setMaximum (Math.max(1, message_buffer.length)) + } + + override def adjustmentValueChanged (e : AdjustmentEvent) = { + //event-handling has to be so general (without UNIT_INCR,...) + // because all events could be sent as TRACK e.g. on my mac + message_no = e.getValue + update_view + } + + // handle Component-Events + override def componentShown(e: ComponentEvent){} + override def componentHidden(e: ComponentEvent){} + override def componentMoved(e: ComponentEvent){} + override def componentResized(e: ComponentEvent){ + // remove all hidden messages from cache + // TODO: move to unlayouted cache + message_cache = message_cache filter ( pair => pair match {case (no, _) => + no <= message_no && no >= message_no - message_view.getComponents.length}) + //calculate preferred size for each panel + message_cache foreach (pair => pair match { case (_, pa) => + calculate_preferred_size (pa) + }) + update_view + } + + //register somewhere + // TODO: only testing atm + Plugin.plugin.stateUpdate.add(state => { + var i = 0 + if(state != null) while (i < 500) { + add_message(state.document) + i += 1 + } + }) +} + +