25 val WAITING = Value("waiting") |
25 val WAITING = Value("waiting") |
26 val RUNNING = Value("running") |
26 val RUNNING = Value("running") |
27 val FINISHED = Value("finished") |
27 val FINISHED = Value("finished") |
28 } |
28 } |
29 |
29 |
30 sealed case class Result(output: List[XML.Tree] = Nil, ok: Boolean = true) |
30 sealed case class Result(failed: Boolean = false, output: List[XML.Tree] = Nil) |
31 |
31 |
32 object State { |
32 object State { |
33 val empty: State = State() |
33 val empty: State = State() |
34 def finish(result: Result): State = State(ok = result.ok, output = result.output) |
34 def finish(result: Result): State = State(failed = result.failed, output = result.output) |
35 } |
35 } |
36 |
36 |
37 sealed case class State( |
37 sealed case class State( |
38 progress: Progress = new Progress, |
38 progress: Progress = new Progress, |
39 process: Future[Unit] = Future.value(()), |
39 process: Future[Unit] = Future.value(()), |
40 ok: Boolean = true, |
40 failed: Boolean = false, |
41 output: List[XML.Tree] = Nil, |
41 output: List[XML.Tree] = Nil, |
42 status: Status.Value = Status.FINISHED |
42 status: Status.Value = Status.FINISHED |
43 ) |
43 ) |
44 } |
44 } |
45 |
45 |
67 process_indicator.update("Running document build process ...", 15) |
67 process_indicator.update("Running document build process ...", 15) |
68 case Document_Dockable.Status.FINISHED => |
68 case Document_Dockable.Status.FINISHED => |
69 process_indicator.update(null, 0) |
69 process_indicator.update(null, 0) |
70 } |
70 } |
71 |
71 |
72 if (!st.ok && output_page != null) message_pane.selection.page = output_page |
72 if (st.failed && output_page != null) message_pane.selection.page = output_page |
73 } |
73 } |
74 |
74 |
75 |
75 |
76 /* text area with zoom/resize */ |
76 /* text area with zoom/resize */ |
77 |
77 |
135 Exn.capture { |
135 Exn.capture { |
136 progress.echo("Start " + Date.now()) |
136 progress.echo("Start " + Date.now()) |
137 Time.seconds(2.0).sleep() |
137 Time.seconds(2.0).sleep() |
138 progress.echo("Stop " + Date.now()) |
138 progress.echo("Stop " + Date.now()) |
139 } |
139 } |
140 val (ok, msg) = |
140 val (failed, msg) = |
141 res match { |
141 res match { |
142 case Exn.Res(_) => (true, Protocol.make_message(XML.string("OK"))) |
142 case Exn.Res(_) => (false, Protocol.make_message(XML.string("OK"))) |
143 case Exn.Exn(exn) => (false, Protocol.error_message(XML.string(Exn.message(exn)))) |
143 case Exn.Exn(exn) => (true, Protocol.error_message(XML.string(Exn.message(exn)))) |
144 } |
144 } |
145 val result = Document_Dockable.Result(ok = ok, output = List(msg)) |
145 val result = Document_Dockable.Result(failed = failed, output = List(msg)) |
146 finish(result) |
146 finish(result) |
147 } |
147 } |
148 st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING) |
148 st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING) |
149 } |
149 } |
150 else st |
150 else st |