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