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