# HG changeset patch
# User wenzelm
# Date 1252237227 -7200
# Node ID 4f023df5a655c2e30707cd188c5be731e6dbbc8a
# Parent  2f0c18f9b6c7c96a9c45a347416431c2412dafdf
tuned;

diff -r 2f0c18f9b6c7 -r 4f023df5a655 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Sep 06 13:31:22 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Sep 06 13:40:27 2009 +0200
@@ -10,7 +10,6 @@
 import isabelle.Isabelle_Process.Result
 import isabelle.renderer.UserAgent
 
-
 import scala.collection.mutable
 
 import java.awt.{BorderLayout, Adjustable, Dimension}
@@ -26,24 +25,29 @@
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-trait Renderer[U, R] {
+trait Renderer[U, R]
+{
   def render (u: U): R
   //relayout a rendered element using argument a
-  def relayout (r: R, a: Int)
+  def relayout(r: R, a: Int)
 }
 
-trait Unrendered[U] {
-  def addUnrendered (id: Int, u: U) : Unit
-  def getUnrendered (id: Int) : Option[U]
-  def size : Int
+trait Unrendered[U]
+{
+  def addUnrendered(id: Int, u: U): Unit
+  def getUnrendered(id: Int): Option[U]
+  def size: Int
 }
 
-trait Rendered[U, R] {
-  def getRendered (id: Int) : Option[R]
-  val renderer : Renderer[U, R]
+trait Rendered[U, R]
+{
+  def getRendered(id: Int): Option[R]
+  val renderer: Renderer[U, R]
 }
 
-class MessagePanel(cache: Rendered[_, XHTMLPanel]) extends JPanel {
+
+class MessagePanel(cache: Rendered[_, XHTMLPanel]) extends JPanel
+{
   // defining the current view
   var offset = 0 //what percentage of the lowest message is hidden
   var no = -1  //index of the lowest message
@@ -53,7 +57,8 @@
   setLayout(null)
   
   // place the bottom of the message at y-coordinate and return the rendered panel
-  def place_message (message_no: Int, y: Int) = {
+  def place_message(message_no: Int, y: Int): XHTMLPanel =
+  {
     //add panel to cache if necessary and possible
     cache.getRendered(message_no) match {
       case Some(panel) => {
@@ -72,7 +77,7 @@
     }
   }
   
-  override def doLayout = {
+  override def doLayout {
     removeAll()
     //calculate offset in pixel
     val panel = place_message(no, 0)
@@ -90,14 +95,16 @@
   }  
 }
 
-class InfoPanel extends JPanel {
+
+class InfoPanel extends JPanel
+{
   val auto_scroll = new JRadioButton("Auto Scroll", false)
   val message_ind = new JTextArea("0")
   add(message_ind)
   add(auto_scroll)
   
   def isAutoScroll = auto_scroll.isSelected
-  def setIndicator(b: Boolean) = {
+  def setIndicator(b: Boolean) {
     message_ind.setBackground(if (b) java.awt.Color.red else java.awt.Color.white)
   }
   def setText(s: String) {
@@ -106,8 +113,9 @@
 }
 
 
-class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener {
-
+class ScrollerDockable(view : View, position : String)
+  extends JPanel with AdjustmentListener
+{
   val renderer:Renderer[Result, XHTMLPanel] = new ResultToPanelRenderer
   val buffer:Unrendered[Result] = new MessageBuffer
   val cache:Rendered[Result, XHTMLPanel] = new PanelCache(buffer, renderer)
@@ -125,16 +133,16 @@
     setPreferredSize(new Dimension(500, 250))
 
   setLayout(new BorderLayout())
-  add (vscroll, BorderLayout.EAST)
-  add (message_panel, BorderLayout.CENTER)
-  add (infopanel, BorderLayout.SOUTH)
+  add(vscroll, BorderLayout.EAST)
+  add(message_panel, BorderLayout.CENTER)
+  add(infopanel, BorderLayout.SOUTH)
   
   // do not show every new message, wait a certain amount of time
   val message_ind_timer : Timer = new Timer(250, new ActionListener {
       // this method is called to indicate a new message
       override def actionPerformed(e:ActionEvent) {
         //fire scroll-event if necessary and wanted
-        if (message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
+        if (message_panel.no != buffer.size * subunits - 1 && infopanel.isAutoScroll) {
           vscroll.setValue(buffer.size*subunits - 1)
         }
         infopanel.setIndicator(false)
@@ -149,7 +157,7 @@
 
     if (!message_ind_timer.isRunning()) {
       if (infopanel.isAutoScroll) {
-        vscroll.setValue(buffer.size*subunits - 1)
+        vscroll.setValue(buffer.size * subunits - 1)
       }
       message_ind_timer.setRepeats(false)
       message_ind_timer.start()
@@ -161,7 +169,7 @@
     }
   }
 
-  override def adjustmentValueChanged (e : AdjustmentEvent) = {
+  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
     if (e.getSource == vscroll) {
@@ -179,8 +187,9 @@
 //Concrete Implementations
 
 //containing the unrendered messages
-class MessageBuffer extends mutable.HashMap[Int,Result] with Unrendered[Result]{
-  override def addUnrendered (id: Int, m: Result) {
+class MessageBuffer extends mutable.HashMap[Int,Result] with Unrendered[Result]
+{
+  override def addUnrendered(id: Int, m: Result) {
     update(id, m)
   }
   override def getUnrendered(id: Int): Option[Result] = {
@@ -192,9 +201,10 @@
 
 //containing the rendered messages
 class PanelCache (buffer: Unrendered[Result], val renderer: Renderer[Result, XHTMLPanel])
-  extends mutable.HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
-
-  override def getRendered (id: Int): Option[XHTMLPanel] = {
+  extends mutable.HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]
+{
+  override def getRendered (id: Int): Option[XHTMLPanel] =
+  {
     //get message from buffer and render it if necessary
     if (!isDefinedAt(id)) {
       buffer.getUnrendered(id) match {
@@ -214,9 +224,10 @@
   }
 }
 
-class ResultToPanelRenderer extends Renderer[Result, XHTMLPanel]{
-  
-  def render (r: Result): XHTMLPanel = {
+class ResultToPanelRenderer extends Renderer[Result, XHTMLPanel]
+{
+  def render(r: Result): XHTMLPanel =
+  {
     val panel = new XHTMLPanel(new UserAgent())
     val fontResolver =
       panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
@@ -235,15 +246,15 @@
     panel
   }
   
-  def relayout (panel: XHTMLPanel, width : Int) {
+  def relayout(panel: XHTMLPanel, width : Int) {
     // ATTENTION:
     // panel has to be displayable in a frame/container message_view for doDocumentLayout to have
     // an effect, especially returning correct preferredSize
-    panel.setBounds (0, 0, width, 1) // document has to fit into width
-    panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then
+    panel.setBounds(0, 0, width, 1) // document has to fit into width
+    panel.doDocumentLayout(panel.getGraphics) //lay out, preferred size is set then
     // if there are thousands of empty panels, all have to be rendered -
     // but this takes time (even for empty panels); therefore minimum size
-    panel.setPreferredSize(new java.awt.Dimension(width, Math.max(25, panel.getPreferredSize.getHeight.toInt)))
+    panel.setPreferredSize(
+      new java.awt.Dimension(width, panel.getPreferredSize.getHeight.toInt max 25))
   }
-
 }
\ No newline at end of file