# HG changeset patch
# User wenzelm
# Date 1443536882 -7200
# Node ID 4d2ea32e0f7503ae9127b6245a87c8a0060c8459
# Parent  c9152a195899be9c5ccd467a08d39344ccb19c57
tuned GUI;

diff -r c9152a195899 -r 4d2ea32e0f75 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Tue Sep 29 15:37:37 2015 +0200
+++ b/src/Pure/GUI/system_dialog.scala	Tue Sep 29 16:28:02 2015 +0200
@@ -8,7 +8,8 @@
 
 
 import java.awt.{GraphicsEnvironment, Point}
-import javax.swing.WindowConstants
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{WindowConstants, JFrame, JDialog}
 import java.io.{File => JFile, BufferedReader, InputStreamReader}
 
 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
@@ -16,7 +17,7 @@
 import scala.swing.event.ButtonClicked
 
 
-class System_Dialog extends Progress
+class System_Dialog(owner: JFrame = null) extends Progress
 {
   /* component state -- owned by GUI thread */
 
@@ -36,9 +37,10 @@
 
         window.pack()
         val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
-        window.location =
-          new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
-        window.visible = true
+        window.setLocation(
+          new Point(point.x - window.getWidth / 2, point.y - window.getHeight / 2))
+
+        window.setVisible(true)
 
         window
       }
@@ -54,7 +56,7 @@
     _window match {
       case None =>
       case Some(window) =>
-        window.visible = false
+        window.setVisible(false)
         window.dispose
         _window = None
     }
@@ -69,10 +71,9 @@
 
   /* window */
 
-  private class Window extends Frame
+  private class Window extends JDialog(owner, _title)
   {
-    title = _title
-    peer.setIconImages(GUI.isabelle_images())
+    setIconImages(GUI.isabelle_images())
 
 
     /* text */
@@ -82,7 +83,7 @@
       columns = 65
       rows = 24
     }
-    if (GUI.is_windows_laf) text.font = (new Label).font
+    text.font = (new Label).font
 
     val scroll_text = new ScrollPane(text)
 
@@ -94,7 +95,7 @@
     layout_panel.layout(scroll_text) = BorderPanel.Position.Center
     layout_panel.layout(action_panel) = BorderPanel.Position.South
 
-    contents = layout_panel
+    setContentPane(layout_panel.peer)
 
     def set_actions(cs: Component*)
     {
@@ -107,12 +108,14 @@
 
     /* close */
 
-    peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
+    setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
 
-    override def closeOperation {
-      if (_return_code.isDefined) conclude()
-      else stopping()
-    }
+    addWindowListener(new WindowAdapter {
+      override def windowClosed(e: WindowEvent) {
+        if (_return_code.isDefined) conclude()
+        else stopping()
+      }
+    })
 
     def stopping()
     {
@@ -162,7 +165,7 @@
   def title(txt: String): Unit =
     GUI_Thread.later {
       _title = txt
-      _window.foreach(window => window.title = txt)
+      _window.foreach(window => window.setTitle(txt))
     }
 
   def return_code(rc: Int): Unit =
@@ -209,4 +212,3 @@
     proc.waitFor
   }
 }
-
diff -r c9152a195899 -r 4d2ea32e0f75 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Tue Sep 29 15:37:37 2015 +0200
+++ b/src/Pure/Tools/main.scala	Tue Sep 29 16:28:02 2015 +0200
@@ -20,7 +20,7 @@
 
   def main(args: Array[String])
   {
-    val system_dialog = new System_Dialog
+    val system_dialog = new System_Dialog()
 
     def exit_error(exn: Throwable): Nothing =
     {
diff -r c9152a195899 -r 4d2ea32e0f75 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Sep 29 15:37:37 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 29 16:28:02 2015 +0200
@@ -266,7 +266,7 @@
 
   def session_build(): Int =
   {
-    val system_dialog = new System_Dialog
+    val system_dialog = new System_Dialog(jEdit.getActiveView())
 
     try {
       val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")