# HG changeset patch # User wenzelm # Date 1386627370 -3600 # Node ID afdb394ee0c03771bce773d19e47c0b695936cad # Parent 8e71c6ed4d747bf419b32d86e73e71407f45fa4f# Parent 87402674fe2f01288416b1f558b0282c3dfe1134 merged diff -r 8e71c6ed4d74 -r afdb394ee0c0 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Mon Dec 09 22:49:27 2013 +0100 +++ b/src/Pure/GUI/gui.scala Mon Dec 09 23:16:10 2013 +0100 @@ -13,6 +13,7 @@ import java.awt.geom.AffineTransform import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow} +import scala.collection.convert.WrapAsJava import scala.swing.{ComboBox, TextArea, ScrollPane} import scala.swing.event.SelectionChanged @@ -129,8 +130,15 @@ def isabelle_icon(): ImageIcon = new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif")) + def isabelle_icons(): List[ImageIcon] = + for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif")) + yield new ImageIcon(getClass.getClassLoader.getResource(icon)) + def isabelle_image(): Image = isabelle_icon().getImage + def isabelle_images(): java.util.List[Image] = + WrapAsJava.seqAsJavaList(isabelle_icons.map(_.getImage)) + /* component hierachy */ diff -r 8e71c6ed4d74 -r afdb394ee0c0 src/Pure/GUI/system_dialog.scala --- a/src/Pure/GUI/system_dialog.scala Mon Dec 09 22:49:27 2013 +0100 +++ b/src/Pure/GUI/system_dialog.scala Mon Dec 09 23:16:10 2013 +0100 @@ -72,7 +72,7 @@ private class Window extends Frame { title = _title - iconImage = GUI.isabelle_image() + peer.setIconImages(GUI.isabelle_images()) /* text */ diff -r 8e71c6ed4d74 -r afdb394ee0c0 src/Pure/build-jars --- a/src/Pure/build-jars Mon Dec 09 22:49:27 2013 +0100 +++ b/src/Pure/build-jars Mon Dec 09 23:16:10 2013 +0100 @@ -221,6 +221,7 @@ echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/. + cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/. isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \ fail "Failed to produce $TARGET"