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