more scalable GUI;
authorwenzelm
Fri, 21 Aug 2015 18:46:12 +0200
changeset 60998 42cebb02b5ae
parent 60997 65cbc1abfc54
child 60999 42c61f0b5748
more scalable GUI;
src/Pure/GUI/gui.scala
src/Pure/GUI/system_dialog.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 */
 
--- 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)