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