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