equal
deleted
inserted
replaced
63 override def stopped: Boolean = |
63 override def stopped: Boolean = |
64 Swing_Thread.now { val b = is_stopped; is_stopped = false; b } |
64 Swing_Thread.now { val b = is_stopped; is_stopped = false; b } |
65 } |
65 } |
66 |
66 |
67 |
67 |
68 /* actions */ |
68 /* action button */ |
69 |
69 |
70 val cancel = new Button("Cancel") { |
70 var button_action: () => Unit = (() => is_stopped = true) |
71 reactions += { case ButtonClicked(_) => is_stopped = true } |
71 val button = new Button("Cancel") { |
|
72 reactions += { case ButtonClicked(_) => button_action() } |
|
73 } |
|
74 def button_exit(rc: Int) |
|
75 { |
|
76 button.text = if (rc == 0) "OK" else "Exit" |
|
77 button_action = (() => sys.exit(rc)) |
72 } |
78 } |
73 |
79 |
74 val actions = new FlowPanel(FlowPanel.Alignment.Center)(cancel) |
80 val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button) |
75 |
81 |
76 |
82 |
77 /* layout panel */ |
83 /* layout panel */ |
78 |
84 |
79 val layout_panel = new BorderPanel |
85 val layout_panel = new BorderPanel |
80 layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center |
86 layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center |
81 layout_panel.layout(actions) = BorderPanel.Position.South |
87 layout_panel.layout(action_panel) = BorderPanel.Position.South |
82 |
88 |
83 contents = layout_panel |
89 contents = layout_panel |
84 |
90 |
85 |
91 |
86 /* main build */ |
92 /* main build */ |
94 ("", |
100 ("", |
95 Build.build(progress, build_heap = true, |
101 Build.build(progress, build_heap = true, |
96 system_mode = system_mode, sessions = List(session))) |
102 system_mode = system_mode, sessions = List(session))) |
97 } |
103 } |
98 catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
104 catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
99 if (rc == 0) { |
105 Swing_Thread.now { |
100 progress.echo("OK\n") |
106 progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
101 Thread.sleep(1000) |
107 button_exit(rc) |
102 } |
108 } |
103 else |
|
104 Swing_Thread.now { |
|
105 Library.error_dialog(this.peer, "Isabelle build failure", |
|
106 Library.scrollable_text(out + "Return code: " + rc + "\n")) |
|
107 } |
|
108 sys.exit(rc) |
|
109 }) |
109 }) |
110 } |
110 } |
111 } |
111 } |
112 |
112 |