src/Pure/GUI/system_dialog.scala
author wenzelm
Tue, 24 Sep 2013 20:41:28 +0200
changeset 53853 e8430d668f44
parent 53783 f5e9d182f645
child 54379 4fac53028f87
permissions -rw-r--r--
more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
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
53853
e8430d668f44 more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
wenzelm
parents: 53783
diff changeset
     2
    Module:     PIDE-GUI
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
     4
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
     5
Dialog for system processes, with optional output window.
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
     8
package isabelle
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
     9
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    10
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    11
import java.awt.{GraphicsEnvironment, Point, Font}
53455
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
    12
import javax.swing.WindowConstants
53460
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
    13
import java.io.{File => JFile, BufferedReader, InputStreamReader}
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    14
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    15
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
53458
ddefd18d5ed0 tuned imports;
wenzelm
parents: 53457
diff changeset
    16
  BorderPanel, Frame, TextArea, Component, Label}
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    17
import scala.swing.event.ButtonClicked
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    18
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    19
53454
1a0c39c728a1 clarified result;
wenzelm
parents: 53453
diff changeset
    20
class System_Dialog extends Build.Progress
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    21
{
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    22
  /* GUI state -- owned by Swing thread */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    23
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    24
  private var _title = "Isabelle"
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    25
  private var _window: Option[Window] = None
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    26
  private var _return_code: Option[Int] = None
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    27
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    28
  private def check_window(): Window =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    29
  {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    30
    Swing_Thread.require()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    31
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    32
    _window match {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    33
      case Some(window) => window
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    34
      case None =>
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    35
        val window = new Window
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    36
        _window = Some(window)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    37
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    38
        window.pack()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    39
        val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    40
        window.location =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    41
          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
    42
        window.visible = true
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    43
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    44
        window
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
  }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    47
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    48
  private val result = Future.promise[Int]
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    49
53454
1a0c39c728a1 clarified result;
wenzelm
parents: 53453
diff changeset
    50
  private def conclude()
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    51
  {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    52
    Swing_Thread.require()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    53
    require(_return_code.isDefined)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    54
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    55
    _window match {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    56
      case None =>
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    57
      case Some(window) =>
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    58
        window.visible = false
53457
b7c15885fd1e more robust exit;
wenzelm
parents: 53456
diff changeset
    59
        window.dispose
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    60
        _window = None
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    61
    }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    62
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    63
    try { result.fulfill(_return_code.get) }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    64
    catch { case ERROR(_) => }
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    65
  }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    66
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    67
  def join(): Int = result.join
53460
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
    68
  def join_exit(): Nothing = sys.exit(join)
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
    69
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    70
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    71
  /* window */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    72
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    73
  private class Window extends Frame
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    74
  {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    75
    title = _title
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    76
    iconImage = GUI.isabelle_image()
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    79
    /* text */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    80
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    81
    val text = new TextArea {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    82
      font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    83
      editable = false
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    84
      columns = 50
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    85
      rows = 20
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    88
    val scroll_text = new ScrollPane(text)
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    91
    /* layout panel with dynamic actions */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    92
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    93
    val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    94
    val layout_panel = new BorderPanel
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    95
    layout_panel.layout(scroll_text) = BorderPanel.Position.Center
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    96
    layout_panel.layout(action_panel) = BorderPanel.Position.South
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    97
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    98
    contents = layout_panel
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
    99
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   100
    def set_actions(cs: Component*)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   101
    {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   102
      action_panel.contents.clear
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   103
      action_panel.contents ++= cs
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   104
      layout_panel.revalidate
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   105
      layout_panel.repaint
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   108
53455
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   109
    /* close */
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   110
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   111
    peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   112
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   113
    override def closeOperation {
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   114
      if (_return_code.isDefined) conclude()
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   115
      else stopping()
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   116
    }
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   117
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   118
    def stopping()
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   119
    {
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   120
      is_stopped = true
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   121
      set_actions(new Label("Stopping ..."))
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   122
    }
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   123
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   124
    val stop_button = new Button("Stop") {
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   125
      reactions += { case ButtonClicked(_) => stopping() }
e9a3390217b3 clarified close operations;
wenzelm
parents: 53454
diff changeset
   126
    }
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   127
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   128
    var do_auto_close = true
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   129
    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
   130
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   131
    val auto_close = new CheckBox("Auto close") {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   132
      reactions += {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   133
        case ButtonClicked(_) => do_auto_close = this.selected
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   134
        if (can_auto_close) conclude()
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
    }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   137
    auto_close.selected = do_auto_close
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   138
    auto_close.tooltip = "Automatically close dialog when finished"
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   139
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   140
    set_actions(stop_button, auto_close)
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   143
    /* exit */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   144
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   145
    val delay_exit =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   146
      Swing_Thread.delay_first(Time.seconds(1.0))
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   147
      {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   148
        if (can_auto_close) conclude()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   149
        else {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   150
          val button =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   151
            new Button(if (_return_code == Some(0)) "OK" else "Exit") {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   152
              reactions += { case ButtonClicked(_) => conclude() }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   153
            }
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   154
          set_actions(button)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   155
          button.peer.getRootPane.setDefaultButton(button.peer)
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   161
  /* progress operations */
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   162
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   163
  def title(txt: String): Unit =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   164
    Swing_Thread.later {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   165
      _title = txt
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   166
      _window.foreach(window => window.title = txt)
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   169
  def return_code(rc: Int): Unit =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   170
    Swing_Thread.later {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   171
      _return_code = Some(rc)
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
   172
      _window match {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
   173
        case None => conclude()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
   174
        case Some(window) => window.delay_exit.invoke
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53455
diff changeset
   175
      }
53453
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   178
  override def echo(txt: String): Unit =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   179
    Swing_Thread.later {
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   180
      val window = check_window()
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   181
      window.text.append(txt + "\n")
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   182
      val vertical = window.scroll_text.peer.getVerticalScrollBar
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   183
      vertical.setValue(vertical.getMaximum)
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
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   186
  override def theory(session: String, theory: String): Unit =
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   187
    echo(session + ": theory " + theory)
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   188
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   189
  @volatile private var is_stopped = false
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   190
  override def stopped: Boolean = is_stopped
53460
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   191
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   192
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   193
  /* system operations */
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   194
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   195
  def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   196
  {
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   197
    val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   198
    proc.getOutputStream.close
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   199
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   200
    val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   201
    try {
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   202
      var line = stdout.readLine
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   203
      while (line != null) {
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   204
        echo(line)
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   205
        line = stdout.readLine
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   206
      }
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   207
    }
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   208
    finally { stdout.close }
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   209
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   210
    proc.waitFor
6015a663b889 tuned signature;
wenzelm
parents: 53458
diff changeset
   211
  }
53453
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   212
}
20ff79162ff3 dialog for system processes, with optional output window;
wenzelm
parents:
diff changeset
   213