evade ugly default font, notably on Windows laf;
authorwenzelm
Wed, 05 Dec 2012 20:43:02 +0100
changeset 50378 72367327bab2
parent 50377 fe4bc5b2abb4
child 50379 a8b0d3729a69
evade ugly default font, notably on Windows laf;
src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Wed Dec 05 20:24:49 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Wed Dec 05 20:43:02 2012 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.awt.{GraphicsEnvironment, Point}
+import java.awt.{GraphicsEnvironment, Point, Font}
 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
   BorderPanel, MainFrame, TextArea, SwingApplication}
 import scala.swing.event.ButtonClicked
@@ -55,6 +55,7 @@
     /* text */
 
     val text = new TextArea {
+      font = new Font("SansSerif", Font.PLAIN, 14)
       editable = false
       columns = 40
       rows = 10