author | wenzelm |
Thu, 17 Aug 2023 20:06:24 +0200 | |
changeset 78536 | 555bdac7c279 |
parent 78535 | af37e1b4dce0 |
child 78537 | 0a4e3e3a55d0 |
permissions | -rw-r--r-- |
61276 | 1 |
/* Title: Pure/System/progress.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Progress context for system processes. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
73897 | 10 |
import java.util.{Map => JMap} |
64201 | 11 |
import java.io.{File => JFile} |
12 |
||
78155 | 13 |
import scala.collection.immutable.SortedMap |
14 |
||
64201 | 15 |
|
75393 | 16 |
object Progress { |
78503 | 17 |
/* output */ |
18 |
||
19 |
sealed abstract class Output { def message: Message } |
|
78155 | 20 |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
21 |
object Kind extends Enumeration { val writeln, warning, error_message = Value } |
78503 | 22 |
sealed case class Message( |
23 |
kind: Kind.Value, |
|
24 |
text: String, |
|
25 |
verbose: Boolean = false |
|
26 |
) extends Output { |
|
27 |
override def message: Message = this |
|
28 |
||
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
29 |
def output_text: String = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
30 |
kind match { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
31 |
case Kind.writeln => Output.writeln_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
32 |
case Kind.warning => Output.warning_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
33 |
case Kind.error_message => Output.error_message_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
34 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
35 |
|
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
36 |
override def toString: String = output_text |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
37 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
38 |
|
78503 | 39 |
sealed case class Theory( |
40 |
theory: String, |
|
41 |
session: String = "", |
|
42 |
percentage: Option[Int] = None |
|
43 |
) extends Output { |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
44 |
def message: Message = |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
45 |
Message(Kind.writeln, print_session + print_theory + print_percentage, verbose = true) |
68987 | 46 |
|
77504 | 47 |
def print_session: String = if_proper(session, session + ": ") |
68987 | 48 |
def print_theory: String = "theory " + theory |
49 |
def print_percentage: String = |
|
50 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 51 |
} |
78155 | 52 |
|
53 |
||
54 |
/* SQL data model */ |
|
55 |
||
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
56 |
object private_data extends SQL.Data("isabelle_progress") { |
78170
c85eeff78b33
proper support for SQLite: avoid conflicts on transaction_lock;
wenzelm
parents:
78156
diff
changeset
|
57 |
val database: Path = Path.explode("$ISABELLE_HOME_USER/progress.db") |
c85eeff78b33
proper support for SQLite: avoid conflicts on transaction_lock;
wenzelm
parents:
78156
diff
changeset
|
58 |
|
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78170
diff
changeset
|
59 |
override lazy val tables = SQL.Tables(Base.table, Agents.table, Messages.table) |
78155 | 60 |
|
61 |
object Base { |
|
62 |
val context_uuid = SQL.Column.string("context_uuid").make_primary_key |
|
63 |
val context = SQL.Column.long("context").make_primary_key |
|
64 |
val stopped = SQL.Column.bool("stopped") |
|
65 |
||
78266 | 66 |
val table = make_table(List(context_uuid, context, stopped)) |
78155 | 67 |
} |
68 |
||
69 |
object Agents { |
|
70 |
val agent_uuid = SQL.Column.string("agent_uuid").make_primary_key |
|
71 |
val context_uuid = SQL.Column.string("context_uuid").make_primary_key |
|
78240 | 72 |
val kind = SQL.Column.string("kind") |
78155 | 73 |
val hostname = SQL.Column.string("hostname") |
74 |
val java_pid = SQL.Column.long("java_pid") |
|
75 |
val java_start = SQL.Column.date("java_start") |
|
76 |
val start = SQL.Column.date("start") |
|
77 |
val stamp = SQL.Column.date("stamp") |
|
78 |
val stop = SQL.Column.date("stop") |
|
79 |
val seen = SQL.Column.long("seen") |
|
80 |
||
78266 | 81 |
val table = |
82 |
make_table( |
|
83 |
List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen), |
|
84 |
name = "agents") |
|
78155 | 85 |
} |
86 |
||
87 |
object Messages { |
|
88 |
type T = SortedMap[Long, Message] |
|
89 |
val empty: T = SortedMap.empty |
|
90 |
||
91 |
val context = SQL.Column.long("context").make_primary_key |
|
92 |
val serial = SQL.Column.long("serial").make_primary_key |
|
93 |
val kind = SQL.Column.int("kind") |
|
94 |
val text = SQL.Column.string("text") |
|
95 |
val verbose = SQL.Column.bool("verbose") |
|
96 |
||
78266 | 97 |
val table = make_table(List(context, serial, kind, text, verbose), name = "messages") |
78155 | 98 |
} |
99 |
||
100 |
def read_progress_context(db: SQL.Database, context_uuid: String): Option[Long] = |
|
101 |
db.execute_query_statementO( |
|
102 |
Base.table.select(List(Base.context), |
|
103 |
sql = Base.context_uuid.where_equal(context_uuid)), _.long(Base.context)) |
|
104 |
||
105 |
def next_progress_context(db: SQL.Database): Long = |
|
106 |
db.execute_query_statementO( |
|
107 |
Base.table.select(List(Base.context.max)), _.long(Base.context)).getOrElse(0L) + 1L |
|
108 |
||
109 |
def read_progress_stopped(db: SQL.Database, context: Long): Boolean = |
|
110 |
db.execute_query_statementO( |
|
111 |
Base.table.select(List(Base.stopped), sql = Base.context.where_equal(context)), |
|
112 |
_.bool(Base.stopped) |
|
113 |
).getOrElse(false) |
|
114 |
||
115 |
def write_progress_stopped(db: SQL.Database, context: Long, stopped: Boolean): Unit = |
|
116 |
db.execute_statement( |
|
117 |
Base.table.update(List(Base.stopped), sql = Base.context.where_equal(context)), |
|
118 |
body = { stmt => stmt.bool(1) = stopped }) |
|
119 |
||
120 |
def update_agent( |
|
121 |
db: SQL.Database, |
|
122 |
agent_uuid: String, |
|
123 |
seen: Long, |
|
78246
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
124 |
stop_now: Boolean = false |
78155 | 125 |
): Unit = { |
78246
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
126 |
val sql = Agents.agent_uuid.where_equal(agent_uuid) |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
127 |
|
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
128 |
val stop = |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
129 |
db.execute_query_statementO( |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
130 |
Agents.table.select(List(Agents.stop), sql = sql), _.get_date(Agents.stop)).flatten |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
131 |
|
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
132 |
db.execute_statement( |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
133 |
Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen), sql = sql), |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
134 |
body = { stmt => |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
135 |
val now = db.now() |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
136 |
stmt.date(1) = now |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
137 |
stmt.date(2) = if (stop_now) Some(now) else stop |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
138 |
stmt.long(3) = seen |
76dd9b9cf624
more robust "stop": further "stamp" ticks may happen afterwards;
wenzelm
parents:
78242
diff
changeset
|
139 |
}) |
78155 | 140 |
} |
141 |
||
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
142 |
def read_messages_serial(db: SQL.Database, context: Long): Long = |
78155 | 143 |
db.execute_query_statementO( |
144 |
Messages.table.select( |
|
145 |
List(Messages.serial.max), sql = Base.context.where_equal(context)), |
|
146 |
_.long(Messages.serial) |
|
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
147 |
).getOrElse(0L) |
78155 | 148 |
|
149 |
def read_messages(db: SQL.Database, context: Long, seen: Long = 0): Messages.T = |
|
150 |
db.execute_query_statement( |
|
151 |
Messages.table.select( |
|
152 |
List(Messages.serial, Messages.kind, Messages.text, Messages.verbose), |
|
153 |
sql = |
|
154 |
SQL.where_and( |
|
155 |
Messages.context.ident + " = " + context, |
|
156 |
if (seen <= 0) "" else Messages.serial.ident + " > " + seen)), |
|
157 |
SortedMap.from[Long, Message], |
|
158 |
{ res => |
|
159 |
val serial = res.long(Messages.serial) |
|
160 |
val kind = Kind(res.int(Messages.kind)) |
|
161 |
val text = res.string(Messages.text) |
|
162 |
val verbose = res.bool(Messages.verbose) |
|
163 |
serial -> Message(kind, text, verbose = verbose) |
|
164 |
} |
|
165 |
) |
|
166 |
||
167 |
def write_messages( |
|
168 |
db: SQL.Database, |
|
169 |
context: Long, |
|
170 |
serial: Long, |
|
171 |
message: Message |
|
172 |
): Unit = { |
|
173 |
db.execute_statement(Messages.table.insert(), body = { stmt => |
|
174 |
stmt.long(1) = context |
|
175 |
stmt.long(2) = serial |
|
176 |
stmt.int(3) = message.kind.id |
|
177 |
stmt.string(4) = message.text |
|
178 |
stmt.bool(5) = message.verbose |
|
179 |
}) |
|
180 |
} |
|
181 |
} |
|
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
182 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
183 |
|
75393 | 184 |
class Progress { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
185 |
def verbose: Boolean = false |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
186 |
final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
187 |
|
78432 | 188 |
def output(message: Progress.Message): Unit = {} |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
189 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
190 |
final def echo(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
191 |
output(Progress.Message(Progress.Kind.writeln, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
192 |
final def echo_warning(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
193 |
output(Progress.Message(Progress.Kind.warning, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
194 |
final def echo_error_message(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
195 |
output(Progress.Message(Progress.Kind.error_message, msg, verbose = verbose)) |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
196 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
197 |
final def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg) |
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
198 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
199 |
def theory(theory: Progress.Theory): Unit = output(theory.message) |
73340 | 200 |
def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} |
64909 | 201 |
|
78432 | 202 |
final def capture[A](e: => A, msg: String, err: Throwable => String): Exn.Result[A] = { |
203 |
echo(msg) |
|
204 |
try { Exn.Res(e) } |
|
205 |
catch { case exn: Throwable => echo_error_message(err(exn)); Exn.Exn[A](exn) } |
|
206 |
} |
|
207 |
||
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
208 |
final def timeit[A]( |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
209 |
body: => A, |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
210 |
message: Exn.Result[A] => String = null, |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
211 |
enabled: Boolean = true |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
212 |
): A = Timing.timeit(body, message = message, enabled = enabled, output = echo(_)) |
65921 | 213 |
|
77524 | 214 |
@volatile private var is_stopped = false |
73367 | 215 |
def stop(): Unit = { is_stopped = true } |
75393 | 216 |
def stopped: Boolean = { |
73367 | 217 |
if (Thread.interrupted()) is_stopped = true |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
218 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
219 |
} |
78529
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
220 |
def stopped_local: Boolean = false |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
221 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
222 |
final def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
223 |
final def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() |
61276 | 224 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 225 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
226 |
final def bash(script: String, |
64201 | 227 |
cwd: JFile = null, |
73897 | 228 |
env: JMap[String, String] = Isabelle_System.settings(), |
64201 | 229 |
redirect: Boolean = false, |
65930 | 230 |
echo: Boolean = false, |
72599 | 231 |
watchdog: Time = Time.zero, |
75393 | 232 |
strict: Boolean = true |
233 |
): Process_Result = { |
|
72599 | 234 |
val result = |
235 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
236 |
progress_stdout = echo_if(echo, _), |
|
237 |
progress_stderr = echo_if(echo, _), |
|
238 |
watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)), |
|
239 |
strict = strict) |
|
240 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 241 |
} |
61276 | 242 |
} |
243 |
||
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
244 |
class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false) |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
245 |
extends Progress { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
246 |
override def output(message: Progress.Message): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
247 |
if (do_output(message)) { |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
248 |
Output.output(message.output_text, stdout = !stderr, include_empty = true) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
249 |
} |
77503 | 250 |
|
251 |
override def toString: String = super.toString + ": console" |
|
61276 | 252 |
} |
65888 | 253 |
|
77507 | 254 |
class File_Progress(path: Path, override val verbose: Boolean = false) |
255 |
extends Progress { |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
256 |
override def output(message: Progress.Message): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
257 |
if (do_output(message)) File.append(path, message.output_text + "\n") |
65888 | 258 |
|
77503 | 259 |
override def toString: String = super.toString + ": " + path.toString |
65888 | 260 |
} |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
261 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
262 |
|
78155 | 263 |
/* database progress */ |
264 |
||
265 |
class Database_Progress( |
|
78532 | 266 |
db: SQL.Database, |
267 |
base_progress: Progress, |
|
78536
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
268 |
input_messages: Boolean = false, |
78532 | 269 |
output_stopped: Boolean = false, |
270 |
kind: String = "progress", |
|
271 |
hostname: String = Isabelle_System.hostname(), |
|
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
272 |
context_uuid: String = UUID.random().toString, |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
273 |
timeout: Option[Time] = None) |
78155 | 274 |
extends Progress { |
275 |
database_progress => |
|
276 |
||
277 |
private var _agent_uuid: String = "" |
|
78382 | 278 |
private var _context: Long = -1 |
78504 | 279 |
private var _serial: Long = 0 |
78529
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
280 |
private var _stopped_db: Boolean = false |
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
281 |
private var _consumer: Consumer_Thread[Progress.Output] = null |
78155 | 282 |
|
283 |
def agent_uuid: String = synchronized { _agent_uuid } |
|
284 |
||
285 |
private def init(): Unit = synchronized { |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
286 |
Progress.private_data.transaction_lock(db, create = true, label = "Database_Progress.init") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
287 |
Progress.private_data.read_progress_context(db, context_uuid) match { |
78155 | 288 |
case Some(context) => |
289 |
_context = context |
|
290 |
_agent_uuid = UUID.random().toString |
|
291 |
case None => |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
292 |
_context = Progress.private_data.next_progress_context(db) |
78155 | 293 |
_agent_uuid = context_uuid |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
294 |
db.execute_statement(Progress.private_data.Base.table.insert(), { stmt => |
78155 | 295 |
stmt.string(1) = context_uuid |
296 |
stmt.long(2) = _context |
|
297 |
stmt.bool(3) = false |
|
298 |
}) |
|
299 |
} |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
300 |
db.execute_statement(Progress.private_data.Agents.table.insert(), { stmt => |
78155 | 301 |
val java = ProcessHandle.current() |
302 |
val java_pid = java.pid |
|
303 |
val java_start = Date.instant(java.info.startInstant.get) |
|
304 |
val now = db.now() |
|
305 |
||
306 |
stmt.string(1) = _agent_uuid |
|
307 |
stmt.string(2) = context_uuid |
|
78240 | 308 |
stmt.string(3) = kind |
309 |
stmt.string(4) = hostname |
|
310 |
stmt.long(5) = java_pid |
|
311 |
stmt.date(6) = java_start |
|
78155 | 312 |
stmt.date(7) = now |
78240 | 313 |
stmt.date(8) = now |
314 |
stmt.date(9) = None |
|
315 |
stmt.long(10) = 0L |
|
78155 | 316 |
}) |
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78170
diff
changeset
|
317 |
} |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
318 |
if (context_uuid == _agent_uuid) db.vacuum(Progress.private_data.tables.list) |
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
319 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
320 |
_consumer = Consumer_Thread.fork_bulk[Progress.Output](name = "Database_Progress.consumer")( |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
321 |
bulk = _ => true, timeout = timeout, |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
322 |
consume = { bulk_output => |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
323 |
sync_database { |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
324 |
_serial = _serial max Progress.private_data.read_messages_serial(db, _context) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
325 |
val serial0 = _serial |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
326 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
327 |
for (out <- bulk_output) { |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
328 |
_serial += 1L |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
329 |
Progress.private_data.write_messages(db, _context, _serial, out.message) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
330 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
331 |
out match { |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
332 |
case message: Progress.Message => |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
333 |
if (do_output(message)) base_progress.output(message) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
334 |
case theory: Progress.Theory => base_progress.theory(theory) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
335 |
} |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
336 |
} |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
337 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
338 |
if (_serial != serial0) Progress.private_data.update_agent(db, _agent_uuid, _serial) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
339 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
340 |
(bulk_output.map(_ => Exn.Res(())), true) |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
341 |
} |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
342 |
}) |
78155 | 343 |
} |
344 |
||
78242 | 345 |
def exit(close: Boolean = false): Unit = synchronized { |
78155 | 346 |
if (_context > 0) { |
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
347 |
_consumer.shutdown() |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
348 |
_consumer = null |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
349 |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
350 |
Progress.private_data.transaction_lock(db, label = "Database_Progress.exit") { |
78504 | 351 |
Progress.private_data.update_agent(db, _agent_uuid, _serial, stop_now = true) |
78155 | 352 |
} |
353 |
_context = 0 |
|
354 |
} |
|
78242 | 355 |
if (close) db.close() |
78155 | 356 |
} |
357 |
||
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
358 |
private def sync_context[A](body: => A): A = synchronized { |
78382 | 359 |
if (_context < 0) throw new IllegalStateException("Database_Progress before init") |
360 |
if (_context == 0) throw new IllegalStateException("Database_Progress after exit") |
|
361 |
||
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
362 |
body |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
363 |
} |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
364 |
|
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
365 |
private def sync_database[A](body: => A): A = { |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78389
diff
changeset
|
366 |
Progress.private_data.transaction_lock(db, label = "Database_Progress.sync") { |
78529
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
367 |
_stopped_db = Progress.private_data.read_progress_stopped(db, _context) |
78155 | 368 |
|
78529
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
369 |
if (_stopped_db && !base_progress.stopped) base_progress.stop() |
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
370 |
if (!_stopped_db && base_progress.stopped && output_stopped) { |
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
371 |
Progress.private_data.write_progress_stopped(db, _context, true) |
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
372 |
} |
78155 | 373 |
|
78536
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
374 |
val serial0 = _serial |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
375 |
if (input_messages) { |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
376 |
val messages = Progress.private_data.read_messages(db, _context, seen = _serial) |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
377 |
for ((message_serial, message) <- messages) { |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
378 |
if (base_progress.do_output(message)) base_progress.output(message) |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
379 |
_serial = _serial max message_serial |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
380 |
} |
78155 | 381 |
} |
78536
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
382 |
else { |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
383 |
_serial = _serial max Progress.private_data.read_messages_serial(db, _context) |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
384 |
} |
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
385 |
|
555bdac7c279
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
wenzelm
parents:
78535
diff
changeset
|
386 |
if (_serial != serial0) Progress.private_data.update_agent(db, _agent_uuid, _serial) |
78155 | 387 |
|
388 |
body |
|
389 |
} |
|
390 |
} |
|
391 |
||
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
392 |
private def sync(): Unit = sync_database {} |
78155 | 393 |
|
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
394 |
override def output(message: Progress.Message): Unit = sync_context { _consumer.send(message) } |
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
395 |
override def theory(theory: Progress.Theory): Unit = sync_context { _consumer.send(theory) } |
78155 | 396 |
|
397 |
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = |
|
398 |
base_progress.nodes_status(nodes_status) |
|
399 |
||
400 |
override def verbose: Boolean = base_progress.verbose |
|
401 |
||
78535
af37e1b4dce0
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
wenzelm
parents:
78532
diff
changeset
|
402 |
override def stop(): Unit = sync_context { base_progress.stop(); sync() } |
78155 | 403 |
override def stopped: Boolean = sync_database { base_progress.stopped } |
78529
0e79fa88cab6
build_worker is stopped independently from master build_process;
wenzelm
parents:
78505
diff
changeset
|
404 |
override def stopped_local: Boolean = sync_database { base_progress.stopped && !_stopped_db } |
78155 | 405 |
|
406 |
override def toString: String = super.toString + ": database " + db |
|
407 |
||
408 |
init() |
|
409 |
sync() |
|
410 |
} |
|
411 |
||
412 |
||
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
413 |
/* structured program progress */ |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
414 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
415 |
object Program_Progress { |
77174 | 416 |
class Program private[Program_Progress](heading: String, title: String) { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
417 |
private val output_buffer = new StringBuffer(256) // synchronized |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
418 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
419 |
def output(message: Progress.Message): Unit = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
420 |
if (output_buffer.length() > 0) output_buffer.append('\n') |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
421 |
output_buffer.append(message.output_text) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
422 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
423 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
424 |
val start_time: Time = Time.now() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
425 |
private var stop_time: Option[Time] = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
426 |
def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) } |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
427 |
|
77174 | 428 |
def output(): (Command.Results, XML.Body) = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
429 |
val output_text = output_buffer.toString |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
430 |
val elapsed_time = stop_time.map(t => t - start_time) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
431 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
432 |
val message_prefix = heading + " " |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
433 |
val message_suffix = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
434 |
elapsed_time match { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
435 |
case None => " ..." |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
436 |
case Some(t) => " ... (" + t.message + " elapsed time)" |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
437 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
438 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
439 |
val (results, message) = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
440 |
if (output_text.isEmpty) { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
441 |
(Command.Results.empty, XML.string(message_prefix + title + message_suffix)) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
442 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
443 |
else { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
444 |
val i = Document_ID.make() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
445 |
val results = Command.Results.make(List(i -> Protocol.writeln_message(output_text))) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
446 |
val message = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
447 |
XML.string(message_prefix) ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
448 |
List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
449 |
XML.string(message_suffix) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
450 |
(results, message) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
451 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
452 |
|
76997 | 453 |
(results, List(XML.elem(Markup.TRACING_MESSAGE, message))) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
454 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
455 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
456 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
457 |
|
77174 | 458 |
abstract class Program_Progress( |
459 |
default_heading: String = "Running", |
|
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
460 |
default_title: String = "program", |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
461 |
override val verbose: Boolean = false |
77174 | 462 |
) extends Progress { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
463 |
private var _finished_programs: List[Program_Progress.Program] = Nil |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
464 |
private var _running_program: Option[Program_Progress.Program] = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
465 |
|
77174 | 466 |
def output(): (Command.Results, XML.Body) = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
467 |
val programs = (_running_program.toList ::: _finished_programs).reverse |
77174 | 468 |
val programs_output = programs.map(_.output()) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
469 |
val results = Command.Results.merge(programs_output.map(_._1)) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
470 |
val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
471 |
(results, body) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
472 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
473 |
|
77174 | 474 |
private def start_program(heading: String, title: String): Unit = synchronized { |
475 |
_running_program = Some(new Program_Progress.Program(heading, title)) |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
476 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
477 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
478 |
def stop_program(): Unit = synchronized { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
479 |
_running_program match { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
480 |
case Some(program) => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
481 |
program.stop_now() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
482 |
_finished_programs ::= program |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
483 |
_running_program = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
484 |
case None => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
485 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
486 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
487 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
488 |
def detect_program(s: String): Option[String] |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
489 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
490 |
override def output(message: Progress.Message): Unit = synchronized { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
491 |
val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else "" |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
492 |
detect_program(writeln_msg).map(Word.explode) match { |
77174 | 493 |
case Some(a :: bs) => |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
494 |
stop_program() |
77174 | 495 |
start_program(a, Word.implode(bs)) |
496 |
case _ => |
|
497 |
if (_running_program.isEmpty) start_program(default_heading, default_title) |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
498 |
if (do_output(message)) _running_program.get.output(message) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
499 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
500 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
501 |
} |