# 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)