src/Tools/jEdit/src/session_build.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62973 744266e32612
child 65256 c3d6dd17d626
permissions -rw-r--r--
tuned signature;
wenzelm@61288
     1
/*  Title:      Tools/jEdit/src/session_build.scala
wenzelm@61288
     2
    Author:     Makarius
wenzelm@61288
     3
wenzelm@61288
     4
Session build management.
wenzelm@61288
     5
*/
wenzelm@61288
     6
wenzelm@61288
     7
package isabelle.jedit
wenzelm@61288
     8
wenzelm@61288
     9
wenzelm@61288
    10
import isabelle._
wenzelm@61288
    11
wenzelm@61288
    12
import java.awt.event.{WindowEvent, WindowAdapter}
wenzelm@61288
    13
import javax.swing.{WindowConstants, JDialog}
wenzelm@61288
    14
wenzelm@61288
    15
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
wenzelm@61288
    16
  BorderPanel, TextArea, Component, Label}
wenzelm@61288
    17
import scala.swing.event.ButtonClicked
wenzelm@61288
    18
wenzelm@61288
    19
import org.gjt.sp.jedit.View
wenzelm@61288
    20
wenzelm@61288
    21
wenzelm@61288
    22
object Session_Build
wenzelm@61288
    23
{
wenzelm@61288
    24
  def session_build(view: View)
wenzelm@61288
    25
  {
wenzelm@61288
    26
    GUI_Thread.require {}
wenzelm@61288
    27
wenzelm@61288
    28
    try {
wenzelm@62973
    29
      if (JEdit_Sessions.session_build_mode() == "none" ||
wenzelm@62973
    30
          JEdit_Sessions.session_build(no_build = true) == 0) JEdit_Sessions.session_start()
wenzelm@61288
    31
      else new Dialog(view)
wenzelm@61288
    32
    }
wenzelm@61288
    33
    catch {
wenzelm@61288
    34
      case exn: Throwable =>
wenzelm@61288
    35
        GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
wenzelm@61288
    36
    }
wenzelm@61288
    37
  }
wenzelm@61288
    38
wenzelm@61288
    39
  private class Dialog(view: View) extends JDialog(view)
wenzelm@61288
    40
  {
wenzelm@61288
    41
    /* text */
wenzelm@61288
    42
wenzelm@61288
    43
    private val text = new TextArea {
wenzelm@61288
    44
      editable = false
wenzelm@61288
    45
      columns = 65
wenzelm@61288
    46
      rows = 24
wenzelm@61288
    47
    }
wenzelm@61742
    48
    text.font = GUI.copy_font((new Label).font)
wenzelm@61288
    49
wenzelm@61288
    50
    private val scroll_text = new ScrollPane(text)
wenzelm@61288
    51
wenzelm@61288
    52
wenzelm@61288
    53
    /* progress */
wenzelm@61288
    54
wenzelm@61288
    55
    @volatile private var is_stopped = false
wenzelm@61288
    56
wenzelm@61288
    57
    private val progress = new Progress {
wenzelm@61288
    58
      override def echo(txt: String): Unit =
wenzelm@61288
    59
        GUI_Thread.later {
wenzelm@61288
    60
          text.append(txt + "\n")
wenzelm@61288
    61
          val vertical = scroll_text.peer.getVerticalScrollBar
wenzelm@61288
    62
          vertical.setValue(vertical.getMaximum)
wenzelm@61288
    63
        }
wenzelm@61288
    64
wenzelm@61288
    65
      override def theory(session: String, theory: String): Unit =
wenzelm@61288
    66
        echo(session + ": theory " + theory)
wenzelm@61288
    67
wenzelm@61288
    68
      override def stopped: Boolean = is_stopped
wenzelm@61288
    69
    }
wenzelm@61288
    70
wenzelm@61288
    71
wenzelm@61288
    72
    /* layout panel with dynamic actions */
wenzelm@61288
    73
wenzelm@61288
    74
    private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
wenzelm@61288
    75
    private val layout_panel = new BorderPanel
wenzelm@61288
    76
    layout_panel.layout(scroll_text) = BorderPanel.Position.Center
wenzelm@61288
    77
    layout_panel.layout(action_panel) = BorderPanel.Position.South
wenzelm@61288
    78
wenzelm@61288
    79
    setContentPane(layout_panel.peer)
wenzelm@61288
    80
wenzelm@61288
    81
    private def set_actions(cs: Component*)
wenzelm@61288
    82
    {
wenzelm@61288
    83
      action_panel.contents.clear
wenzelm@61288
    84
      action_panel.contents ++= cs
wenzelm@61288
    85
      layout_panel.revalidate
wenzelm@61288
    86
      layout_panel.repaint
wenzelm@61288
    87
    }
wenzelm@61288
    88
wenzelm@61288
    89
wenzelm@61288
    90
    /* return code and exit */
wenzelm@61288
    91
wenzelm@61288
    92
    private var _return_code: Option[Int] = None
wenzelm@61288
    93
wenzelm@61288
    94
    private def return_code(rc: Int): Unit =
wenzelm@61288
    95
      GUI_Thread.later {
wenzelm@61288
    96
        _return_code = Some(rc)
wenzelm@61288
    97
        delay_exit.invoke
wenzelm@61288
    98
      }
wenzelm@61288
    99
wenzelm@61288
   100
    private val delay_exit =
wenzelm@61288
   101
      GUI_Thread.delay_first(Time.seconds(1.0))
wenzelm@61288
   102
      {
wenzelm@61288
   103
        if (can_auto_close) conclude()
wenzelm@61288
   104
        else {
wenzelm@61299
   105
          val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
wenzelm@61288
   106
          set_actions(button)
wenzelm@61288
   107
          button.peer.getRootPane.setDefaultButton(button.peer)
wenzelm@61288
   108
        }
wenzelm@61288
   109
      }
wenzelm@61288
   110
wenzelm@61288
   111
    private def conclude()
wenzelm@61288
   112
    {
wenzelm@61288
   113
      setVisible(false)
wenzelm@61288
   114
      dispose()
wenzelm@61288
   115
    }
wenzelm@61288
   116
wenzelm@61288
   117
wenzelm@61288
   118
    /* close */
wenzelm@61288
   119
wenzelm@61288
   120
    setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
wenzelm@61288
   121
wenzelm@61288
   122
    addWindowListener(new WindowAdapter {
wenzelm@61288
   123
      override def windowClosing(e: WindowEvent) {
wenzelm@61288
   124
        if (_return_code.isDefined) conclude()
wenzelm@61288
   125
        else stopping()
wenzelm@61288
   126
      }
wenzelm@61288
   127
    })
wenzelm@61288
   128
wenzelm@61288
   129
    private def stopping()
wenzelm@61288
   130
    {
wenzelm@61288
   131
      is_stopped = true
wenzelm@61288
   132
      set_actions(new Label("Stopping ..."))
wenzelm@61288
   133
    }
wenzelm@61288
   134
wenzelm@61288
   135
    private val stop_button = new Button("Stop") {
wenzelm@61288
   136
      reactions += { case ButtonClicked(_) => stopping() }
wenzelm@61288
   137
    }
wenzelm@61288
   138
wenzelm@61288
   139
    private var do_auto_close = true
wenzelm@61288
   140
    private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
wenzelm@61288
   141
wenzelm@61288
   142
    private val auto_close = new CheckBox("Auto close") {
wenzelm@61288
   143
      reactions += {
wenzelm@61288
   144
        case ButtonClicked(_) => do_auto_close = this.selected
wenzelm@61288
   145
        if (can_auto_close) conclude()
wenzelm@61288
   146
      }
wenzelm@61288
   147
    }
wenzelm@61288
   148
    auto_close.selected = do_auto_close
wenzelm@61288
   149
    auto_close.tooltip = "Automatically close dialog when finished"
wenzelm@61288
   150
wenzelm@61288
   151
    set_actions(stop_button, auto_close)
wenzelm@61288
   152
wenzelm@61288
   153
wenzelm@61288
   154
    /* main */
wenzelm@61288
   155
wenzelm@61288
   156
    setTitle("Isabelle build (" +
wenzelm@61288
   157
      Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
wenzelm@61288
   158
      "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
wenzelm@61288
   159
wenzelm@61288
   160
    pack()
wenzelm@61288
   161
    setLocationRelativeTo(view)
wenzelm@61288
   162
    setVisible(true)
wenzelm@61288
   163
wenzelm@61556
   164
    Standard_Thread.fork("session_build") {
wenzelm@62973
   165
      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name() + " ...")
wenzelm@61288
   166
wenzelm@61288
   167
      val (out, rc) =
wenzelm@62973
   168
        try { ("", JEdit_Sessions.session_build(progress = progress)) }
wenzelm@61288
   169
        catch {
wenzelm@61288
   170
          case exn: Throwable =>
wenzelm@61288
   171
            (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
wenzelm@61288
   172
        }
wenzelm@61288
   173
wenzelm@61288
   174
      progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
wenzelm@61289
   175
wenzelm@62973
   176
      if (rc == 0) JEdit_Sessions.session_start()
wenzelm@61680
   177
      else progress.echo("Session build failed -- prover process remains inactive!")
wenzelm@61288
   178
wenzelm@61288
   179
      return_code(rc)
wenzelm@61288
   180
    }
wenzelm@61288
   181
  }
wenzelm@61288
   182
}