17 import scala.swing.event.ButtonClicked |
17 import scala.swing.event.ButtonClicked |
18 |
18 |
19 import org.gjt.sp.jedit.View |
19 import org.gjt.sp.jedit.View |
20 |
20 |
21 |
21 |
22 object Session_Build |
22 object Session_Build { |
23 { |
23 def check_dialog(view: View): Unit = { |
24 def check_dialog(view: View): Unit = |
|
25 { |
|
26 val options = PIDE.options.value |
24 val options = PIDE.options.value |
27 Isabelle_Thread.fork() { |
25 Isabelle_Thread.fork() { |
28 try { |
26 try { |
29 if (JEdit_Sessions.session_no_build || |
27 if (JEdit_Sessions.session_no_build || |
30 JEdit_Sessions.session_build(options, no_build = true) == 0) |
28 JEdit_Sessions.session_build(options, no_build = true) == 0) |
76 layout_panel.layout(scroll_text) = BorderPanel.Position.Center |
73 layout_panel.layout(scroll_text) = BorderPanel.Position.Center |
77 layout_panel.layout(action_panel) = BorderPanel.Position.South |
74 layout_panel.layout(action_panel) = BorderPanel.Position.South |
78 |
75 |
79 setContentPane(layout_panel.peer) |
76 setContentPane(layout_panel.peer) |
80 |
77 |
81 private def set_actions(cs: Component*): Unit = |
78 private def set_actions(cs: Component*): Unit = { |
82 { |
|
83 action_panel.contents.clear() |
79 action_panel.contents.clear() |
84 action_panel.contents ++= cs |
80 action_panel.contents ++= cs |
85 layout_panel.revalidate() |
81 layout_panel.revalidate() |
86 layout_panel.repaint() |
82 layout_panel.repaint() |
87 } |
83 } |
96 _return_code = Some(rc) |
92 _return_code = Some(rc) |
97 delay_exit.invoke() |
93 delay_exit.invoke() |
98 } |
94 } |
99 |
95 |
100 private val delay_exit = |
96 private val delay_exit = |
101 Delay.first(Time.seconds(1.0), gui = true) |
97 Delay.first(Time.seconds(1.0), gui = true) { |
102 { |
|
103 if (can_auto_close) conclude() |
98 if (can_auto_close) conclude() |
104 else { |
99 else { |
105 val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } |
100 val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } |
106 set_actions(button) |
101 set_actions(button) |
107 button.peer.getRootPane.setDefaultButton(button.peer) |
102 button.peer.getRootPane.setDefaultButton(button.peer) |
108 } |
103 } |
109 } |
104 } |
110 |
105 |
111 private def conclude(): Unit = |
106 private def conclude(): Unit = { |
112 { |
|
113 setVisible(false) |
107 setVisible(false) |
114 dispose() |
108 dispose() |
115 } |
109 } |
116 |
110 |
117 |
111 |
118 /* close */ |
112 /* close */ |
119 |
113 |
120 setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) |
114 setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) |
121 |
115 |
122 addWindowListener(new WindowAdapter { |
116 addWindowListener(new WindowAdapter { |
123 override def windowClosing(e: WindowEvent): Unit = |
117 override def windowClosing(e: WindowEvent): Unit = { |
124 { |
|
125 if (_return_code.isDefined) conclude() |
118 if (_return_code.isDefined) conclude() |
126 else stopping() |
119 else stopping() |
127 } |
120 } |
128 }) |
121 }) |
129 |
122 |
130 private def stopping(): Unit = |
123 private def stopping(): Unit = { |
131 { |
|
132 progress.stop() |
124 progress.stop() |
133 set_actions(new Label("Stopping ...")) |
125 set_actions(new Label("Stopping ...")) |
134 } |
126 } |
135 |
127 |
136 private val stop_button = new Button("Stop") { |
128 private val stop_button = new Button("Stop") { |