# HG changeset patch # User wenzelm # Date 1419936634 -3600 # Node ID 702e0971d61763487057ac62c320b5176caaea58 # Parent ff6954c847e286e53c59272e87051200f32d8ef1 added system property isabelle.laf, notably for initial system dialog; let L&F take care of font scaling, e.g. GTK+ for Linux where X11 dpi scaling does not really work; diff -r ff6954c847e2 -r 702e0971d617 NEWS --- a/NEWS Tue Dec 30 10:38:10 2014 +0100 +++ b/NEWS Tue Dec 30 11:50:34 2014 +0100 @@ -254,6 +254,10 @@ * JVM system property "isabelle.threads" determines size of Scala thread pool, like Isabelle system option "threads" for ML. +* JVM system property "isabelle.laf" determines the default Swing +look-and-feel, via internal class name or symbolic name as in the jEdit +menu Global Options / Appearance. + * System option "pretty_margin" is superseded by "thy_output_margin", which is also accessible via document antiquotation option "margin". Only the margin for document output may be changed, but not the global diff -r ff6954c847e2 -r 702e0971d617 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Tue Dec 30 10:38:10 2014 +0100 +++ b/src/Pure/GUI/gui.scala Tue Dec 30 11:50:34 2014 +0100 @@ -25,14 +25,19 @@ { /* Swing look-and-feel */ + def find_laf(name: String): Option[String] = + UIManager.getInstalledLookAndFeels(). + find(c => c.getName == name || c.getClassName == name). + map(_.getClassName) + def get_laf(): String = - { - if (Platform.is_windows || Platform.is_macos) - UIManager.getSystemLookAndFeelClassName() - else - UIManager.getInstalledLookAndFeels().find(_.getName == "Nimbus").map(_.getClassName) - .getOrElse(UIManager.getCrossPlatformLookAndFeelClassName()) - } + find_laf(System.getProperty("isabelle.laf")) getOrElse { + if (Platform.is_windows || Platform.is_macos) + UIManager.getSystemLookAndFeelClassName() + else + find_laf("Nimbus") getOrElse + UIManager.getCrossPlatformLookAndFeelClassName() + } def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) @@ -161,12 +166,6 @@ else "" + HTML.encode(text) + "" - /* screen resolution */ - - def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72 - def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt - - /* icon */ def isabelle_icon(): ImageIcon = diff -r ff6954c847e2 -r 702e0971d617 src/Pure/GUI/system_dialog.scala --- a/src/Pure/GUI/system_dialog.scala Tue Dec 30 10:38:10 2014 +0100 +++ b/src/Pure/GUI/system_dialog.scala Tue Dec 30 11:50:34 2014 +0100 @@ -78,7 +78,6 @@ /* text */ val text = new TextArea { - font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14) editable = false columns = 50 rows = 20