src/Tools/jEdit/src/jedit/LazyScroller.scala

correct resizing of xhtml-panels

/*
 * 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 vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1)
  vscroll.addAdjustmentListener(this)
  add (vscroll, BorderLayout.EAST)
  add (message_view, 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()
    val rendered_message = render (message_buffer(message_no))
    val resizable = new JScrollPane(rendered_message, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER)
    message_view.add (resizable)
  }
  
  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 < 1000) {
          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
    }
 }