separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
tuned signature;
--- a/src/Pure/System/gui_setup.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/System/gui_setup.scala Thu Apr 04 17:47:28 2013 +0200
@@ -23,7 +23,7 @@
}
def top = new MainFrame {
- iconImage = Isabelle_System.get_icon().getImage
+ iconImage = GUI.isabelle_image()
title = "Isabelle setup"
--- a/src/Pure/System/isabelle_system.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Apr 04 17:47:28 2013 +0200
@@ -11,7 +11,6 @@
import java.util.regex.Pattern
import java.io.{File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter}
-import javax.swing.ImageIcon
import scala.util.matching.Regex
@@ -421,10 +420,4 @@
case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
}
}
-
-
- /* icon */
-
- def get_icon(): ImageIcon =
- new ImageIcon(platform_path(Path.explode("~~/lib/logo/isabelle.gif")))
}
--- a/src/Pure/Tools/build_dialog.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala Thu Apr 04 17:47:28 2013 +0200
@@ -64,7 +64,7 @@
more_dirs: List[(Boolean, Path)],
session: String): MainFrame = new MainFrame
{
- iconImage = Isabelle_System.get_icon().getImage
+ iconImage = GUI.isabelle_image()
/* GUI state */
--- a/src/Pure/Tools/ml_statistics.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/Tools/ml_statistics.scala Thu Apr 04 17:47:28 2013 +0200
@@ -134,7 +134,7 @@
ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
Swing_Thread.later {
new Frame {
- iconImage = Isabelle_System.get_icon().getImage
+ iconImage = GUI.isabelle_image()
title = name
contents = Component.wrap(new ChartPanel(c))
visible = true
--- a/src/Pure/Tools/task_statistics.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/Tools/task_statistics.scala Thu Apr 04 17:47:28 2013 +0200
@@ -53,7 +53,7 @@
def show_frame(bins: Int = 100): Unit =
Swing_Thread.later {
new Frame {
- iconImage = Isabelle_System.get_icon().getImage
+ iconImage = GUI.isabelle_image()
title = name
contents = Component.wrap(new ChartPanel(chart(bins)))
visible = true
--- a/src/Pure/build-jars Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Pure/build-jars Thu Apr 04 17:47:28 2013 +0200
@@ -42,6 +42,7 @@
System/color_value.scala
System/command_line.scala
System/event_bus.scala
+ System/gui.scala
System/gui_setup.scala
System/html5_panel.scala
System/interrupt.scala
--- a/src/Tools/Graphview/src/graphview.scala Thu Apr 04 17:33:04 2013 +0200
+++ b/src/Tools/Graphview/src/graphview.scala Thu Apr 04 17:47:28 2013 +0200
@@ -37,7 +37,7 @@
catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
val top = new MainFrame {
- iconImage = Isabelle_System.get_icon().getImage
+ iconImage = GUI.isabelle_image()
title = "Graphview"
minimumSize = new Dimension(640, 480)