# HG changeset patch
# User wenzelm
# Date 1440175572 -7200
# Node ID 42cebb02b5ae378d0a599ff66eb43ac800e22b0b
# Parent  65cbc1abfc549a10ecf9425914f24fa254cc47f2
more scalable GUI;

diff -r 65cbc1abfc54 -r 42cebb02b5ae src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Aug 21 17:59:54 2015 +0200
+++ b/src/Pure/GUI/gui.scala	Fri Aug 21 18:46:12 2015 +0200
@@ -44,6 +44,10 @@
     Platform.is_macos &&
     UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
 
+  def is_windows_laf(): Boolean =
+    Platform.is_windows &&
+    UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
+
 
   /* plain focus traversal, notably for text fields */
 
diff -r 65cbc1abfc54 -r 42cebb02b5ae src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Fri Aug 21 17:59:54 2015 +0200
+++ b/src/Pure/GUI/system_dialog.scala	Fri Aug 21 18:46:12 2015 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.awt.{GraphicsEnvironment, Point, Font}
+import java.awt.{GraphicsEnvironment, Point}
 import javax.swing.WindowConstants
 import java.io.{File => JFile, BufferedReader, InputStreamReader}
 
@@ -82,6 +82,7 @@
       columns = 65
       rows = 24
     }
+    if (GUI.is_windows_laf) text.font = (new Label).font
 
     val scroll_text = new ScrollPane(text)