equal
deleted
inserted
replaced
11 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics} |
11 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics} |
12 import java.awt.geom.AffineTransform |
12 import java.awt.geom.AffineTransform |
13 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog, |
13 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog, |
14 JButton, JTextField, JLabel} |
14 JButton, JTextField, JLabel} |
15 |
15 |
|
16 |
|
17 import scala.collection.JavaConverters |
16 import scala.swing.{ComboBox, TextArea, ScrollPane} |
18 import scala.swing.{ComboBox, TextArea, ScrollPane} |
17 import scala.swing.event.SelectionChanged |
19 import scala.swing.event.SelectionChanged |
18 |
20 |
19 |
21 |
20 object GUI |
22 object GUI |
214 |
216 |
215 def line_metrics(font: Font): LineMetrics = |
217 def line_metrics(font: Font): LineMetrics = |
216 font.getLineMetrics("", new FontRenderContext(null, false, false)) |
218 font.getLineMetrics("", new FontRenderContext(null, false, false)) |
217 |
219 |
218 def transform_font(font: Font, transform: AffineTransform): Font = |
220 def transform_font(font: Font, transform: AffineTransform): Font = |
219 { |
221 font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) |
220 import scala.collection.JavaConversions._ |
|
221 font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform))) |
|
222 } |
|
223 |
222 |
224 def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = |
223 def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = |
225 new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
224 new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
226 |
225 |
227 def label_font(): Font = (new JLabel).getFont |
226 def label_font(): Font = (new JLabel).getFont |