--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/system_dialog.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,212 @@
+/* Title: Pure/GUI/system_dialog.scala
+ Author: Makarius
+
+Dialog for system processes, with optional output window.
+*/
+
+package isabelle
+
+
+import java.awt.{GraphicsEnvironment, Point, Font}
+import javax.swing.WindowConstants
+import java.io.{File => JFile, BufferedReader, InputStreamReader}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, Frame, TextArea, Component, Label}
+import scala.swing.event.ButtonClicked
+
+
+class System_Dialog 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
+ }
+ }
+
+ private val result = Future.promise[Int]
+
+ private def conclude()
+ {
+ Swing_Thread.require()
+ require(_return_code.isDefined)
+
+ _window match {
+ case None =>
+ case Some(window) =>
+ window.visible = false
+ window.dispose
+ _window = None
+ }
+
+ try { result.fulfill(_return_code.get) }
+ catch { case ERROR(_) => }
+ }
+
+ def join(): Int = result.join
+ def join_exit(): Nothing = sys.exit(join)
+
+
+ /* window */
+
+ private class Window extends Frame
+ {
+ title = _title
+ iconImage = GUI.isabelle_image()
+
+
+ /* 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
+ }
+
+
+ /* close */
+
+ peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
+
+ override def closeOperation {
+ if (_return_code.isDefined) conclude()
+ else stopping()
+ }
+
+ def stopping()
+ {
+ is_stopped = true
+ set_actions(new Label("Stopping ..."))
+ }
+
+ val stop_button = new Button("Stop") {
+ reactions += { case ButtonClicked(_) => stopping() }
+ }
+
+ 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"
+
+ 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 match {
+ case None => conclude()
+ case Some(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
+
+
+ /* system operations */
+
+ def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
+ {
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ proc.getOutputStream.close
+
+ val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+ try {
+ var line = stdout.readLine
+ while (line != null) {
+ echo(line)
+ line = stdout.readLine
+ }
+ }
+ finally { stdout.close }
+
+ proc.waitFor
+ }
+}
+