src/Pure/GUI/system_dialog.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
child 59201 702e0971d617
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
wenzelm@53783
     1
/*  Title:      Pure/GUI/system_dialog.scala
wenzelm@53453
     2
    Author:     Makarius
wenzelm@53453
     3
wenzelm@53453
     4
Dialog for system processes, with optional output window.
wenzelm@53453
     5
*/
wenzelm@53453
     6
wenzelm@53453
     7
package isabelle
wenzelm@53453
     8
wenzelm@53453
     9
wenzelm@53453
    10
import java.awt.{GraphicsEnvironment, Point, Font}
wenzelm@53455
    11
import javax.swing.WindowConstants
wenzelm@53460
    12
import java.io.{File => JFile, BufferedReader, InputStreamReader}
wenzelm@53453
    13
wenzelm@53453
    14
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
wenzelm@53458
    15
  BorderPanel, Frame, TextArea, Component, Label}
wenzelm@53453
    16
import scala.swing.event.ButtonClicked
wenzelm@53453
    17
wenzelm@53453
    18
wenzelm@53454
    19
class System_Dialog extends Build.Progress
wenzelm@53453
    20
{
wenzelm@57612
    21
  /* component state -- owned by GUI thread */
wenzelm@53453
    22
wenzelm@53453
    23
  private var _title = "Isabelle"
wenzelm@53453
    24
  private var _window: Option[Window] = None
wenzelm@53453
    25
  private var _return_code: Option[Int] = None
wenzelm@53453
    26
wenzelm@53453
    27
  private def check_window(): Window =
wenzelm@53453
    28
  {
wenzelm@57612
    29
    GUI_Thread.require {}
wenzelm@53453
    30
wenzelm@53453
    31
    _window match {
wenzelm@53453
    32
      case Some(window) => window
wenzelm@53453
    33
      case None =>
wenzelm@53453
    34
        val window = new Window
wenzelm@53453
    35
        _window = Some(window)
wenzelm@53453
    36
wenzelm@53453
    37
        window.pack()
wenzelm@53453
    38
        val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
wenzelm@53453
    39
        window.location =
wenzelm@53453
    40
          new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
wenzelm@53453
    41
        window.visible = true
wenzelm@53453
    42
wenzelm@53453
    43
        window
wenzelm@53453
    44
      }
wenzelm@53453
    45
  }
wenzelm@53453
    46
wenzelm@53456
    47
  private val result = Future.promise[Int]
wenzelm@53456
    48
wenzelm@53454
    49
  private def conclude()
wenzelm@53453
    50
  {
wenzelm@57612
    51
    GUI_Thread.require {}
wenzelm@53453
    52
    require(_return_code.isDefined)
wenzelm@53453
    53
wenzelm@53453
    54
    _window match {
wenzelm@53453
    55
      case None =>
wenzelm@53453
    56
      case Some(window) =>
wenzelm@53453
    57
        window.visible = false
wenzelm@53457
    58
        window.dispose
wenzelm@53453
    59
        _window = None
wenzelm@53453
    60
    }
wenzelm@53453
    61
wenzelm@53456
    62
    try { result.fulfill(_return_code.get) }
wenzelm@53456
    63
    catch { case ERROR(_) => }
wenzelm@53453
    64
  }
wenzelm@53453
    65
wenzelm@53456
    66
  def join(): Int = result.join
wenzelm@53460
    67
  def join_exit(): Nothing = sys.exit(join)
wenzelm@53456
    68
wenzelm@53453
    69
wenzelm@53453
    70
  /* window */
wenzelm@53453
    71
wenzelm@53453
    72
  private class Window extends Frame
wenzelm@53453
    73
  {
wenzelm@53453
    74
    title = _title
wenzelm@54709
    75
    peer.setIconImages(GUI.isabelle_images())
wenzelm@53453
    76
wenzelm@53453
    77
wenzelm@53453
    78
    /* text */
wenzelm@53453
    79
wenzelm@53453
    80
    val text = new TextArea {
wenzelm@53453
    81
      font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
wenzelm@53453
    82
      editable = false
wenzelm@53453
    83
      columns = 50
wenzelm@53453
    84
      rows = 20
wenzelm@53453
    85
    }
wenzelm@53453
    86
wenzelm@53453
    87
    val scroll_text = new ScrollPane(text)
wenzelm@53453
    88
wenzelm@53453
    89
wenzelm@53453
    90
    /* layout panel with dynamic actions */
wenzelm@53453
    91
wenzelm@53453
    92
    val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
wenzelm@53453
    93
    val layout_panel = new BorderPanel
wenzelm@53453
    94
    layout_panel.layout(scroll_text) = BorderPanel.Position.Center
wenzelm@53453
    95
    layout_panel.layout(action_panel) = BorderPanel.Position.South
wenzelm@53453
    96
wenzelm@53453
    97
    contents = layout_panel
wenzelm@53453
    98
wenzelm@53453
    99
    def set_actions(cs: Component*)
wenzelm@53453
   100
    {
wenzelm@53453
   101
      action_panel.contents.clear
wenzelm@53453
   102
      action_panel.contents ++= cs
wenzelm@53453
   103
      layout_panel.revalidate
wenzelm@53453
   104
      layout_panel.repaint
wenzelm@53453
   105
    }
wenzelm@53453
   106
wenzelm@53453
   107
wenzelm@53455
   108
    /* close */
wenzelm@53455
   109
wenzelm@53455
   110
    peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
wenzelm@53455
   111
wenzelm@53455
   112
    override def closeOperation {
wenzelm@53455
   113
      if (_return_code.isDefined) conclude()
wenzelm@53455
   114
      else stopping()
wenzelm@53455
   115
    }
wenzelm@53455
   116
wenzelm@53455
   117
    def stopping()
wenzelm@53455
   118
    {
wenzelm@53455
   119
      is_stopped = true
wenzelm@53455
   120
      set_actions(new Label("Stopping ..."))
wenzelm@53455
   121
    }
wenzelm@53455
   122
wenzelm@53455
   123
    val stop_button = new Button("Stop") {
wenzelm@53455
   124
      reactions += { case ButtonClicked(_) => stopping() }
wenzelm@53455
   125
    }
wenzelm@53453
   126
wenzelm@53453
   127
    var do_auto_close = true
wenzelm@53453
   128
    def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
wenzelm@53453
   129
wenzelm@53453
   130
    val auto_close = new CheckBox("Auto close") {
wenzelm@53453
   131
      reactions += {
wenzelm@53453
   132
        case ButtonClicked(_) => do_auto_close = this.selected
wenzelm@53453
   133
        if (can_auto_close) conclude()
wenzelm@53453
   134
      }
wenzelm@53453
   135
    }
wenzelm@53453
   136
    auto_close.selected = do_auto_close
wenzelm@53453
   137
    auto_close.tooltip = "Automatically close dialog when finished"
wenzelm@53453
   138
wenzelm@53453
   139
    set_actions(stop_button, auto_close)
wenzelm@53453
   140
wenzelm@53453
   141
wenzelm@53453
   142
    /* exit */
wenzelm@53453
   143
wenzelm@53453
   144
    val delay_exit =
wenzelm@57612
   145
      GUI_Thread.delay_first(Time.seconds(1.0))
wenzelm@53453
   146
      {
wenzelm@53453
   147
        if (can_auto_close) conclude()
wenzelm@53453
   148
        else {
wenzelm@53453
   149
          val button =
wenzelm@53453
   150
            new Button(if (_return_code == Some(0)) "OK" else "Exit") {
wenzelm@53453
   151
              reactions += { case ButtonClicked(_) => conclude() }
wenzelm@53453
   152
            }
wenzelm@53453
   153
          set_actions(button)
wenzelm@53453
   154
          button.peer.getRootPane.setDefaultButton(button.peer)
wenzelm@53453
   155
        }
wenzelm@53453
   156
      }
wenzelm@53453
   157
  }
wenzelm@53453
   158
wenzelm@53453
   159
wenzelm@53453
   160
  /* progress operations */
wenzelm@53453
   161
wenzelm@53453
   162
  def title(txt: String): Unit =
wenzelm@57612
   163
    GUI_Thread.later {
wenzelm@53453
   164
      _title = txt
wenzelm@53453
   165
      _window.foreach(window => window.title = txt)
wenzelm@53453
   166
    }
wenzelm@53453
   167
wenzelm@53453
   168
  def return_code(rc: Int): Unit =
wenzelm@57612
   169
    GUI_Thread.later {
wenzelm@53453
   170
      _return_code = Some(rc)
wenzelm@53456
   171
      _window match {
wenzelm@53456
   172
        case None => conclude()
wenzelm@53456
   173
        case Some(window) => window.delay_exit.invoke
wenzelm@53456
   174
      }
wenzelm@53453
   175
    }
wenzelm@53453
   176
wenzelm@53453
   177
  override def echo(txt: String): Unit =
wenzelm@57612
   178
    GUI_Thread.later {
wenzelm@53453
   179
      val window = check_window()
wenzelm@53453
   180
      window.text.append(txt + "\n")
wenzelm@53453
   181
      val vertical = window.scroll_text.peer.getVerticalScrollBar
wenzelm@53453
   182
      vertical.setValue(vertical.getMaximum)
wenzelm@53453
   183
    }
wenzelm@53453
   184
wenzelm@53453
   185
  override def theory(session: String, theory: String): Unit =
wenzelm@53453
   186
    echo(session + ": theory " + theory)
wenzelm@53453
   187
wenzelm@53453
   188
  @volatile private var is_stopped = false
wenzelm@53453
   189
  override def stopped: Boolean = is_stopped
wenzelm@53460
   190
wenzelm@53460
   191
wenzelm@53460
   192
  /* system operations */
wenzelm@53460
   193
wenzelm@53460
   194
  def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
wenzelm@53460
   195
  {
wenzelm@53460
   196
    val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
wenzelm@53460
   197
    proc.getOutputStream.close
wenzelm@53460
   198
wenzelm@53460
   199
    val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
wenzelm@53460
   200
    try {
wenzelm@53460
   201
      var line = stdout.readLine
wenzelm@53460
   202
      while (line != null) {
wenzelm@53460
   203
        echo(line)
wenzelm@53460
   204
        line = stdout.readLine
wenzelm@53460
   205
      }
wenzelm@53460
   206
    }
wenzelm@53460
   207
    finally { stdout.close }
wenzelm@53460
   208
wenzelm@53460
   209
    proc.waitFor
wenzelm@53460
   210
  }
wenzelm@53453
   211
}
wenzelm@53453
   212