tuned signature;
authorwenzelm
Sun Sep 22 18:36:22 2013 +0200 (2013-09-22)
changeset 53785e64edcc2f8bf
parent 53784 322a3ff42b33
child 53786 064cb0458071
tuned signature;
src/Pure/GUI/gui.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Sun Sep 22 18:07:34 2013 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Sun Sep 22 18:36:22 2013 +0200
     1.3 @@ -7,7 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.awt.{Image, Component, Container, Toolkit, Window}
     1.8 +import java.awt.{Image, Component, Container, Toolkit, Window, Font}
     1.9 +import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    1.10 +import java.awt.geom.AffineTransform
    1.11  import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
    1.12  
    1.13  import scala.swing.{ComboBox, TextArea, ScrollPane}
    1.14 @@ -150,5 +152,23 @@
    1.15        case Some(frame: JFrame) => Some(frame.getLayeredPane)
    1.16        case _ => None
    1.17      }
    1.18 +
    1.19 +
    1.20 +  /* font operations */
    1.21 +
    1.22 +  def font_metrics(font: Font): LineMetrics =
    1.23 +    font.getLineMetrics("", new FontRenderContext(null, false, false))
    1.24 +
    1.25 +  def imitate_font(family: String, font: Font): Font =
    1.26 +  {
    1.27 +    val font1 = new Font(family, font.getStyle, font.getSize)
    1.28 +    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
    1.29 +  }
    1.30 +
    1.31 +  def transform_font(font: Font, transform: AffineTransform): Font =
    1.32 +  {
    1.33 +    import scala.collection.JavaConversions._
    1.34 +    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
    1.35 +  }
    1.36  }
    1.37  
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:07:34 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:36:22 2013 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
     2.5      setColumns(40)
     2.6      setToolTipText(query_label.tooltip)
     2.7 -    setFont(Token_Markup.imitate_font(Rendering.font_family(), getFont))
     2.8 +    setFont(GUI.imitate_font(Rendering.font_family(), getFont))
     2.9    }
    2.10  
    2.11    private case class Context_Entry(val name: String, val description: String)
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 18:07:34 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 18:36:22 2013 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  import isabelle._
     3.5  
     3.6  import java.awt.{Font, Color}
     3.7 -import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
     3.8 +import java.awt.font.TextAttribute
     3.9  import java.awt.geom.AffineTransform
    3.10  
    3.11  import org.gjt.sp.util.SyntaxUtilities
    3.12 @@ -68,24 +68,6 @@
    3.13    }
    3.14  
    3.15  
    3.16 -  /* font operations */
    3.17 -
    3.18 -  private def font_metrics(font: Font): LineMetrics =
    3.19 -    font.getLineMetrics("", new FontRenderContext(null, false, false))
    3.20 -
    3.21 -  def imitate_font(family: String, font: Font): Font =
    3.22 -  {
    3.23 -    val font1 = new Font(family, font.getStyle, font.getSize)
    3.24 -    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
    3.25 -  }
    3.26 -
    3.27 -  def transform_font(font: Font, transform: AffineTransform): Font =
    3.28 -  {
    3.29 -    import scala.collection.JavaConversions._
    3.30 -    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
    3.31 -  }
    3.32 -
    3.33 -
    3.34    /* extended syntax styles */
    3.35  
    3.36    private val plain_range: Int = JEditToken.ID_COUNT
    3.37 @@ -109,10 +91,10 @@
    3.38          val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    3.39  
    3.40          def shift(y: Float): Font =
    3.41 -          transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
    3.42 +          GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
    3.43  
    3.44 -        val m0 = font_metrics(font0)
    3.45 -        val m1 = font_metrics(font1)
    3.46 +        val m0 = GUI.font_metrics(font0)
    3.47 +        val m1 = GUI.font_metrics(font1)
    3.48          val a = m1.getAscent - m0.getAscent
    3.49          val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
    3.50          if (a > 0.0f) shift(a)
    3.51 @@ -145,12 +127,12 @@
    3.52          for (idx <- 0 until max_user_fonts)
    3.53            new_styles(user_font(idx, i.toByte)) = style
    3.54          for ((family, idx) <- Symbol.font_index)
    3.55 -          new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
    3.56 +          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(family, _))
    3.57        }
    3.58        new_styles(hidden) =
    3.59          new SyntaxStyle(hidden_color, null,
    3.60            { val font = styles(0).getFont
    3.61 -            transform_font(new Font(font.getFamily, 0, 1),
    3.62 +            GUI.transform_font(new Font(font.getFamily, 0, 1),
    3.63                AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
    3.64        new_styles
    3.65      }