--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/system_dialog.scala Sat Sep 07 13:59:47 2013 +0200
@@ -0,0 +1,173 @@
+/* Title: Pure/Tools/system_dialog.scala
+ Author: Makarius
+
+Dialog for system processes, with optional output window.
+*/
+
+package isabelle
+
+
+import java.awt.{GraphicsEnvironment, Point, Font}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, Frame, TextArea, SwingApplication, Component, Label}
+import scala.swing.event.ButtonClicked
+
+
+class System_Dialog(continue: Int => Unit) extends Build.Progress
+{
+ /* GUI state -- owned by Swing thread */
+
+ private var _title = "Isabelle"
+ private var _window: Option[Window] = None
+ private var _return_code: Option[Int] = None
+
+ private def check_window(): Window =
+ {
+ Swing_Thread.require()
+
+ _window match {
+ case Some(window) => window
+ case None =>
+ val window = new Window
+ _window = Some(window)
+
+ 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
+ }
+ }
+
+ def conclude()
+ {
+ Swing_Thread.require()
+ require(_return_code.isDefined)
+
+ _window match {
+ case None =>
+ case Some(window) =>
+ window.visible = false
+ _window = None
+ }
+
+ continue(_return_code.get)
+ }
+
+
+ /* window */
+
+ private class Window extends Frame
+ {
+ title = _title
+ iconImage = GUI.isabelle_image()
+
+ override def closeOperation { if (_return_code.isDefined) conclude() }
+
+
+ /* text */
+
+ val text = new TextArea {
+ font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
+ editable = false
+ columns = 50
+ rows = 20
+ }
+
+ val scroll_text = new ScrollPane(text)
+
+
+ /* layout panel with dynamic actions */
+
+ val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
+ val layout_panel = new BorderPanel
+ layout_panel.layout(scroll_text) = BorderPanel.Position.Center
+ layout_panel.layout(action_panel) = BorderPanel.Position.South
+
+ contents = layout_panel
+
+ def set_actions(cs: Component*)
+ {
+ action_panel.contents.clear
+ action_panel.contents ++= cs
+ layout_panel.revalidate
+ layout_panel.repaint
+ }
+
+
+ /* actions */
+
+ var do_auto_close = true
+ def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
+
+ val auto_close = new CheckBox("Auto close") {
+ reactions += {
+ case ButtonClicked(_) => do_auto_close = this.selected
+ if (can_auto_close) conclude()
+ }
+ }
+ auto_close.selected = do_auto_close
+ auto_close.tooltip = "Automatically close dialog when finished"
+
+
+ val stop_button = new Button("Stop") {
+ reactions += {
+ case ButtonClicked(_) =>
+ is_stopped = true
+ set_actions(new Label("Stopping ..."))
+ }
+ }
+
+ set_actions(stop_button, auto_close)
+
+
+ /* exit */
+
+ val delay_exit =
+ Swing_Thread.delay_first(Time.seconds(1.0))
+ {
+ if (can_auto_close) conclude()
+ else {
+ val button =
+ new Button(if (_return_code == Some(0)) "OK" else "Exit") {
+ reactions += { case ButtonClicked(_) => conclude() }
+ }
+ set_actions(button)
+ button.peer.getRootPane.setDefaultButton(button.peer)
+ }
+ }
+ }
+
+
+ /* progress operations */
+
+ def title(txt: String): Unit =
+ Swing_Thread.later {
+ _title = txt
+ _window.foreach(window => window.title = txt)
+ }
+
+ def return_code(rc: Int): Unit =
+ Swing_Thread.later {
+ _return_code = Some(rc)
+ _window.foreach(window => window.delay_exit.invoke)
+ }
+
+ override def echo(txt: String): Unit =
+ Swing_Thread.later {
+ val window = check_window()
+ window.text.append(txt + "\n")
+ val vertical = window.scroll_text.peer.getVerticalScrollBar
+ vertical.setValue(vertical.getMaximum)
+ }
+
+ override def theory(session: String, theory: String): Unit =
+ echo(session + ": theory " + theory)
+
+ @volatile private var is_stopped = false
+ override def stopped: Boolean = is_stopped
+}
+
--- a/src/Pure/build-jars Sat Sep 07 11:36:03 2013 +0200
+++ b/src/Pure/build-jars Sat Sep 07 13:59:47 2013 +0200
@@ -64,6 +64,7 @@
System/session.scala
System/swing_thread.scala
System/system_channel.scala
+ System/system_dialog.scala
System/utf8.scala
Thy/html.scala
Thy/present.scala