1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/wrap_panel.scala	Wed Sep 18 15:09:15 2013 +0200
     1.3 @@ -0,0 +1,113 @@
     1.4 +/*  Title:      Pure/System/wrap_panel.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Panel with improved FlowLayout for wrapping of components over
     1.8 +multiple lines, see also
     1.9 +http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
    1.10 +scala.swing.FlowPanel.
    1.11 +*/
    1.12 +
    1.13 +package isabelle
    1.14 +
    1.15 +
    1.16 +import java.awt.{FlowLayout, Container, Dimension}
    1.17 +import javax.swing.{JPanel, JScrollPane, SwingUtilities}
    1.18 +
    1.19 +import scala.swing.{Panel, FlowPanel, Component, SequentialContainer}
    1.20 +
    1.21 +
    1.22 +object Wrap_Panel
    1.23 +{
    1.24 +  val Alignment = FlowPanel.Alignment
    1.25 +
    1.26 +  class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
    1.27 +    extends FlowLayout(align: Int, hgap: Int, vgap: Int)
    1.28 +  {
    1.29 +    override def preferredLayoutSize(target: Container): Dimension =
    1.30 +      layout_size(target, true)
    1.31 +
    1.32 +    override def minimumLayoutSize(target: Container): Dimension =
    1.33 +    {
    1.34 +      val minimum = layout_size(target, false)
    1.35 +      minimum.width -= (getHgap + 1)
    1.36 +      minimum
    1.37 +    }
    1.38 +
    1.39 +    private def layout_size(target: Container, preferred: Boolean): Dimension =
    1.40 +    {
    1.41 +      target.getTreeLock.synchronized
    1.42 +      {
    1.43 +        val target_width =
    1.44 +          if (target.getSize.width == 0) Integer.MAX_VALUE
    1.45 +          else target.getSize.width
    1.46 +
    1.47 +        val hgap = getHgap
    1.48 +        val vgap = getVgap
    1.49 +        val insets = target.getInsets
    1.50 +        val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
    1.51 +        val max_width = target_width - horizontal_insets_and_gap
    1.52 +
    1.53 +        val dim = new Dimension(0, 0)
    1.54 +        var row_width = 0
    1.55 +        var row_height = 0
    1.56 +        def add_row()
    1.57 +        {
    1.58 +          dim.width = dim.width max row_width
    1.59 +          if (dim.height > 0) dim.height += vgap
    1.60 +          dim.height += row_height
    1.61 +        }
    1.62 +
    1.63 +        for {
    1.64 +          i <- 0 until target.getComponentCount
    1.65 +          m = target.getComponent(i)
    1.66 +          if m.isVisible
    1.67 +          d = if (preferred) m.getPreferredSize else m.getMinimumSize()
    1.68 +        }
    1.69 +        {
    1.70 +          if (row_width + d.width > max_width) {
    1.71 +            add_row()
    1.72 +            row_width = 0
    1.73 +            row_height = 0
    1.74 +          }
    1.75 +
    1.76 +          if (row_width != 0) row_width += hgap
    1.77 +
    1.78 +          row_width += d.width
    1.79 +          row_height = row_height max d.height
    1.80 +        }
    1.81 +        add_row()
    1.82 +
    1.83 +        dim.width += horizontal_insets_and_gap
    1.84 +        dim.height += insets.top + insets.bottom + vgap * 2
    1.85 +
    1.86 +        SwingUtilities.getAncestorOfClass(classOf[JScrollPane], target) match {
    1.87 +          case scroll_pane: Container if target.isValid =>
    1.88 +            dim.width -= (hgap + 1)
    1.89 +          case _ =>
    1.90 +        }
    1.91 +
    1.92 +        dim
    1.93 +      }
    1.94 +    }
    1.95 +  }
    1.96 +}
    1.97 +
    1.98 +
    1.99 +class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
   1.100 +  extends Panel with SequentialContainer.Wrapper
   1.101 +{
   1.102 +  override lazy val peer: JPanel =
   1.103 +    new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
   1.104 +
   1.105 +  def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
   1.106 +  def this() = this(Wrap_Panel.Alignment.Center)()
   1.107 +
   1.108 +  contents ++= contents0
   1.109 +
   1.110 +  private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
   1.111 +
   1.112 +  def vGap: Int = layoutManager.getVgap
   1.113 +  def vGap_=(n: Int) { layoutManager.setVgap(n) }
   1.114 +  def hGap: Int = layoutManager.getHgap
   1.115 +  def hGap_=(n: Int) { layoutManager.setHgap(n) }
   1.116 +}

     2.1 --- a/src/Pure/build-jars	Wed Sep 18 13:31:44 2013 +0200
     2.2 +++ b/src/Pure/build-jars	Wed Sep 18 15:09:15 2013 +0200
     2.3 @@ -65,6 +65,7 @@
     2.4    System/system_channel.scala
     2.5    System/system_dialog.scala
     2.6    System/utf8.scala
     2.7 +  System/wrap_panel.scala
     2.8    Thy/html.scala
     2.9    Thy/present.scala
    2.10    Thy/thy_header.scala

     3.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  import scala.actors.Actor._
     3.6  
     3.7 -import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
     3.8 +import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
     3.9  import scala.swing.event.ButtonClicked
    3.10  
    3.11  import java.awt.BorderLayout
    3.12 @@ -154,7 +154,7 @@
    3.13    }
    3.14  
    3.15    private val controls =
    3.16 -    new FlowPanel(FlowPanel.Alignment.Right)(
    3.17 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    3.18        query_label, Component.wrap(query), context, limit, allow_dups,
    3.19        process_indicator.component, apply_query, zoom)
    3.20    add(controls.peer, BorderLayout.NORTH)

     4.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  import scala.actors.Actor._
     4.6  
     4.7 -import scala.swing.{FlowPanel, Button}
     4.8 +import scala.swing.Button
     4.9  import scala.swing.event.ButtonClicked
    4.10  
    4.11  import java.lang.System
    4.12 @@ -94,7 +94,7 @@
    4.13    private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    4.14    zoom.tooltip = "Zoom factor for basic font size"
    4.15  
    4.16 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
    4.17 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
    4.18    add(controls.peer, BorderLayout.NORTH)
    4.19  
    4.20  

     5.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4  
     5.5  import scala.actors.Actor._
     5.6  
     5.7 -import scala.swing.{FlowPanel, Button, CheckBox}
     5.8 +import scala.swing.{Button, CheckBox}
     5.9  import scala.swing.event.ButtonClicked
    5.10  
    5.11  import java.lang.System
    5.12 @@ -155,6 +155,7 @@
    5.13      }
    5.14    }
    5.15  
    5.16 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
    5.17 +  private val controls =
    5.18 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
    5.19    add(controls.peer, BorderLayout.NORTH)
    5.20  }

     6.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  
     6.5  import scala.actors.Actor._
     6.6  
     6.7 -import scala.swing.{FlowPanel, Button, Component, Label, TextField, CheckBox}
     6.8 +import scala.swing.{Button, Component, Label, TextField, CheckBox}
     6.9  import scala.swing.event.ButtonClicked
    6.10  
    6.11  import java.awt.BorderLayout
    6.12 @@ -174,7 +174,7 @@
    6.13    }
    6.14  
    6.15    private val controls =
    6.16 -    new FlowPanel(FlowPanel.Alignment.Right)(
    6.17 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    6.18        provers_label, Component.wrap(provers), isar_proofs,
    6.19        process_indicator.component, apply_query, cancel_query, locate_query, zoom)
    6.20    add(controls.peer, BorderLayout.NORTH)

     7.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     7.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  import isabelle._
     7.5  
     7.6  import scala.actors.Actor._
     7.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     7.8 +import scala.swing.{Button, TextArea, Label, ListView, Alignment,
     7.9    ScrollPane, Component, CheckBox, BorderPanel}
    7.10  import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
    7.11  
    7.12 @@ -83,7 +83,7 @@
    7.13    private val logic = Isabelle_Logic.logic_selector(true)
    7.14  
    7.15    private val controls =
    7.16 -    new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
    7.17 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
    7.18    add(controls.peer, BorderLayout.NORTH)
    7.19  
    7.20  

     8.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 18 13:31:44 2013 +0200
     8.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4  import isabelle._
     8.5  
     8.6  import scala.actors.Actor._
     8.7 -import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
     8.8 +import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
     8.9  import scala.swing.event.{MouseClicked, ValueChanged}
    8.10  
    8.11  import java.lang.System
    8.12 @@ -142,7 +142,8 @@
    8.13        s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
    8.14    }
    8.15  
    8.16 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
    8.17 +  private val controls =
    8.18 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
    8.19    add(controls.peer, BorderLayout.NORTH)
    8.20  
    8.21