1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/system_dialog.scala	Sat Sep 07 13:59:47 2013 +0200
     1.3 @@ -0,0 +1,173 @@
     1.4 +/*  Title:      Pure/Tools/system_dialog.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Dialog for system processes, with optional output window.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.awt.{GraphicsEnvironment, Point, Font}
    1.14 +
    1.15 +import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
    1.16 +  BorderPanel, Frame, TextArea, SwingApplication, Component, Label}
    1.17 +import scala.swing.event.ButtonClicked
    1.18 +
    1.19 +
    1.20 +class System_Dialog(continue: Int => Unit) extends Build.Progress
    1.21 +{
    1.22 +  /* GUI state -- owned by Swing thread */
    1.23 +
    1.24 +  private var _title = "Isabelle"
    1.25 +  private var _window: Option[Window] = None
    1.26 +  private var _return_code: Option[Int] = None
    1.27 +
    1.28 +  private def check_window(): Window =
    1.29 +  {
    1.30 +    Swing_Thread.require()
    1.31 +
    1.32 +    _window match {
    1.33 +      case Some(window) => window
    1.34 +      case None =>
    1.35 +        val window = new Window
    1.36 +        _window = Some(window)
    1.37 +
    1.38 +        window.pack()
    1.39 +        val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    1.40 +        window.location =
    1.41 +          new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
    1.42 +        window.visible = true
    1.43 +
    1.44 +        window
    1.45 +      }
    1.46 +  }
    1.47 +
    1.48 +  def conclude()
    1.49 +  {
    1.50 +    Swing_Thread.require()
    1.51 +    require(_return_code.isDefined)
    1.52 +
    1.53 +    _window match {
    1.54 +      case None =>
    1.55 +      case Some(window) =>
    1.56 +        window.visible = false
    1.57 +        _window = None
    1.58 +    }
    1.59 +
    1.60 +    continue(_return_code.get)
    1.61 +  }
    1.62 +
    1.63 +
    1.64 +  /* window */
    1.65 +
    1.66 +  private class Window extends Frame
    1.67 +  {
    1.68 +    title = _title
    1.69 +    iconImage = GUI.isabelle_image()
    1.70 +
    1.71 +    override def closeOperation { if (_return_code.isDefined) conclude() }
    1.72 +
    1.73 +
    1.74 +    /* text */
    1.75 +
    1.76 +    val text = new TextArea {
    1.77 +      font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
    1.78 +      editable = false
    1.79 +      columns = 50
    1.80 +      rows = 20
    1.81 +    }
    1.82 +
    1.83 +    val scroll_text = new ScrollPane(text)
    1.84 +
    1.85 +
    1.86 +    /* layout panel with dynamic actions */
    1.87 +
    1.88 +    val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
    1.89 +    val layout_panel = new BorderPanel
    1.90 +    layout_panel.layout(scroll_text) = BorderPanel.Position.Center
    1.91 +    layout_panel.layout(action_panel) = BorderPanel.Position.South
    1.92 +
    1.93 +    contents = layout_panel
    1.94 +
    1.95 +    def set_actions(cs: Component*)
    1.96 +    {
    1.97 +      action_panel.contents.clear
    1.98 +      action_panel.contents ++= cs
    1.99 +      layout_panel.revalidate
   1.100 +      layout_panel.repaint
   1.101 +    }
   1.102 +
   1.103 +
   1.104 +    /* actions */
   1.105 +
   1.106 +    var do_auto_close = true
   1.107 +    def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
   1.108 +
   1.109 +    val auto_close = new CheckBox("Auto close") {
   1.110 +      reactions += {
   1.111 +        case ButtonClicked(_) => do_auto_close = this.selected
   1.112 +        if (can_auto_close) conclude()
   1.113 +      }
   1.114 +    }
   1.115 +    auto_close.selected = do_auto_close
   1.116 +    auto_close.tooltip = "Automatically close dialog when finished"
   1.117 +
   1.118 +
   1.119 +    val stop_button = new Button("Stop") {
   1.120 +      reactions += {
   1.121 +        case ButtonClicked(_) =>
   1.122 +          is_stopped = true
   1.123 +          set_actions(new Label("Stopping ..."))
   1.124 +      }
   1.125 +    }
   1.126 +
   1.127 +    set_actions(stop_button, auto_close)
   1.128 +
   1.129 +
   1.130 +    /* exit */
   1.131 +
   1.132 +    val delay_exit =
   1.133 +      Swing_Thread.delay_first(Time.seconds(1.0))
   1.134 +      {
   1.135 +        if (can_auto_close) conclude()
   1.136 +        else {
   1.137 +          val button =
   1.138 +            new Button(if (_return_code == Some(0)) "OK" else "Exit") {
   1.139 +              reactions += { case ButtonClicked(_) => conclude() }
   1.140 +            }
   1.141 +          set_actions(button)
   1.142 +          button.peer.getRootPane.setDefaultButton(button.peer)
   1.143 +        }
   1.144 +      }
   1.145 +  }
   1.146 +
   1.147 +
   1.148 +  /* progress operations */
   1.149 +
   1.150 +  def title(txt: String): Unit =
   1.151 +    Swing_Thread.later {
   1.152 +      _title = txt
   1.153 +      _window.foreach(window => window.title = txt)
   1.154 +    }
   1.155 +
   1.156 +  def return_code(rc: Int): Unit =
   1.157 +    Swing_Thread.later {
   1.158 +      _return_code = Some(rc)
   1.159 +      _window.foreach(window => window.delay_exit.invoke)
   1.160 +    }
   1.161 +
   1.162 +  override def echo(txt: String): Unit =
   1.163 +    Swing_Thread.later {
   1.164 +      val window = check_window()
   1.165 +      window.text.append(txt + "\n")
   1.166 +      val vertical = window.scroll_text.peer.getVerticalScrollBar
   1.167 +      vertical.setValue(vertical.getMaximum)
   1.168 +    }
   1.169 +
   1.170 +  override def theory(session: String, theory: String): Unit =
   1.171 +    echo(session + ": theory " + theory)
   1.172 +
   1.173 +  @volatile private var is_stopped = false
   1.174 +  override def stopped: Boolean = is_stopped
   1.175 +}
   1.176 +

     2.1 --- a/src/Pure/build-jars	Sat Sep 07 11:36:03 2013 +0200
     2.2 +++ b/src/Pure/build-jars	Sat Sep 07 13:59:47 2013 +0200
     2.3 @@ -64,6 +64,7 @@
     2.4    System/session.scala
     2.5    System/swing_thread.scala
     2.6    System/system_channel.scala
     2.7 +  System/system_dialog.scala
     2.8    System/utf8.scala
     2.9    Thy/html.scala
    2.10    Thy/present.scala