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