author | wenzelm |
Fri, 16 Jun 2023 14:20:18 +0200 | |
changeset 78170 | c85eeff78b33 |
parent 78156 | da5cc332ded3 |
child 78187 | 2df0f3604a67 |
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 { |
78155 | 17 |
/* messages */ |
18 |
||
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
19 |
object Kind extends Enumeration { val writeln, warning, error_message = Value } |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
20 |
sealed case class Message(kind: Kind.Value, text: String, verbose: Boolean = false) { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
21 |
def output_text: String = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
22 |
kind match { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
27 |
|
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
28 |
override def toString: String = output_text |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
29 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
30 |
|
75393 | 31 |
sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
32 |
def message: Message = |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
33 |
Message(Kind.writeln, print_session + print_theory + print_percentage, verbose = true) |
68987 | 34 |
|
77504 | 35 |
def print_session: String = if_proper(session, session + ": ") |
68987 | 36 |
def print_theory: String = "theory " + theory |
37 |
def print_percentage: String = |
|
38 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 39 |
} |
78155 | 40 |
|
41 |
||
42 |
/* SQL data model */ |
|
43 |
||
44 |
object Data { |
|
78170
c85eeff78b33
proper support for SQLite: avoid conflicts on transaction_lock;
wenzelm
parents:
78156
diff
changeset
|
45 |
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
|
46 |
|
78155 | 47 |
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = |
48 |
SQL.Table("isabelle_progress" + if_proper(name, "_" + name), columns, body = body) |
|
49 |
||
50 |
object Base { |
|
51 |
val context_uuid = SQL.Column.string("context_uuid").make_primary_key |
|
52 |
val context = SQL.Column.long("context").make_primary_key |
|
53 |
val stopped = SQL.Column.bool("stopped") |
|
54 |
||
55 |
val table = make_table("", List(context_uuid, context, stopped)) |
|
56 |
} |
|
57 |
||
58 |
object Agents { |
|
59 |
val agent_uuid = SQL.Column.string("agent_uuid").make_primary_key |
|
60 |
val context_uuid = SQL.Column.string("context_uuid").make_primary_key |
|
61 |
val hostname = SQL.Column.string("hostname") |
|
62 |
val java_pid = SQL.Column.long("java_pid") |
|
63 |
val java_start = SQL.Column.date("java_start") |
|
64 |
val start = SQL.Column.date("start") |
|
65 |
val stamp = SQL.Column.date("stamp") |
|
66 |
val stop = SQL.Column.date("stop") |
|
67 |
val seen = SQL.Column.long("seen") |
|
68 |
||
69 |
val table = make_table("agents", |
|
70 |
List(agent_uuid, context_uuid, hostname, java_pid, java_start, start, stamp, stop, seen)) |
|
71 |
} |
|
72 |
||
73 |
object Messages { |
|
74 |
type T = SortedMap[Long, Message] |
|
75 |
val empty: T = SortedMap.empty |
|
76 |
||
77 |
val context = SQL.Column.long("context").make_primary_key |
|
78 |
val serial = SQL.Column.long("serial").make_primary_key |
|
79 |
val kind = SQL.Column.int("kind") |
|
80 |
val text = SQL.Column.string("text") |
|
81 |
val verbose = SQL.Column.bool("verbose") |
|
82 |
||
83 |
val table = make_table("messages", List(context, serial, kind, text, verbose)) |
|
84 |
} |
|
85 |
||
86 |
val all_tables: SQL.Tables = SQL.Tables(Base.table, Agents.table, Messages.table) |
|
87 |
||
88 |
def read_progress_context(db: SQL.Database, context_uuid: String): Option[Long] = |
|
89 |
db.execute_query_statementO( |
|
90 |
Base.table.select(List(Base.context), |
|
91 |
sql = Base.context_uuid.where_equal(context_uuid)), _.long(Base.context)) |
|
92 |
||
93 |
def next_progress_context(db: SQL.Database): Long = |
|
94 |
db.execute_query_statementO( |
|
95 |
Base.table.select(List(Base.context.max)), _.long(Base.context)).getOrElse(0L) + 1L |
|
96 |
||
97 |
def read_progress_stopped(db: SQL.Database, context: Long): Boolean = |
|
98 |
db.execute_query_statementO( |
|
99 |
Base.table.select(List(Base.stopped), sql = Base.context.where_equal(context)), |
|
100 |
_.bool(Base.stopped) |
|
101 |
).getOrElse(false) |
|
102 |
||
103 |
def write_progress_stopped(db: SQL.Database, context: Long, stopped: Boolean): Unit = |
|
104 |
db.execute_statement( |
|
105 |
Base.table.update(List(Base.stopped), sql = Base.context.where_equal(context)), |
|
106 |
body = { stmt => stmt.bool(1) = stopped }) |
|
107 |
||
108 |
def update_agent( |
|
109 |
db: SQL.Database, |
|
110 |
agent_uuid: String, |
|
111 |
seen: Long, |
|
112 |
stop: Boolean = false |
|
113 |
): Unit = { |
|
114 |
val sql = |
|
115 |
Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen), |
|
116 |
sql = Agents.agent_uuid.where_equal(agent_uuid)) |
|
117 |
db.execute_statement(sql, body = { stmt => |
|
118 |
val now = db.now() |
|
119 |
stmt.date(1) = now |
|
120 |
stmt.date(2) = if (stop) Some(now) else None |
|
121 |
stmt.long(3) = seen |
|
122 |
}) |
|
123 |
} |
|
124 |
||
125 |
def next_messages_serial(db: SQL.Database, context: Long): Long = |
|
126 |
db.execute_query_statementO( |
|
127 |
Messages.table.select( |
|
128 |
List(Messages.serial.max), sql = Base.context.where_equal(context)), |
|
129 |
_.long(Messages.serial) |
|
130 |
).getOrElse(0L) + 1L |
|
131 |
||
132 |
def read_messages(db: SQL.Database, context: Long, seen: Long = 0): Messages.T = |
|
133 |
db.execute_query_statement( |
|
134 |
Messages.table.select( |
|
135 |
List(Messages.serial, Messages.kind, Messages.text, Messages.verbose), |
|
136 |
sql = |
|
137 |
SQL.where_and( |
|
138 |
Messages.context.ident + " = " + context, |
|
139 |
if (seen <= 0) "" else Messages.serial.ident + " > " + seen)), |
|
140 |
SortedMap.from[Long, Message], |
|
141 |
{ res => |
|
142 |
val serial = res.long(Messages.serial) |
|
143 |
val kind = Kind(res.int(Messages.kind)) |
|
144 |
val text = res.string(Messages.text) |
|
145 |
val verbose = res.bool(Messages.verbose) |
|
146 |
serial -> Message(kind, text, verbose = verbose) |
|
147 |
} |
|
148 |
) |
|
149 |
||
150 |
def write_messages( |
|
151 |
db: SQL.Database, |
|
152 |
context: Long, |
|
153 |
serial: Long, |
|
154 |
message: Message |
|
155 |
): Unit = { |
|
156 |
db.execute_statement(Messages.table.insert(), body = { stmt => |
|
157 |
stmt.long(1) = context |
|
158 |
stmt.long(2) = serial |
|
159 |
stmt.int(3) = message.kind.id |
|
160 |
stmt.string(4) = message.text |
|
161 |
stmt.bool(5) = message.verbose |
|
162 |
}) |
|
163 |
} |
|
164 |
} |
|
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
165 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
166 |
|
75393 | 167 |
class Progress { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
168 |
def verbose: Boolean = false |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
169 |
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
|
170 |
|
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
171 |
def output(message: Progress.Message) = {} |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
172 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
173 |
final def echo(msg: String, verbose: Boolean = false): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
174 |
output(Progress.Message(Progress.Kind.writeln, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
175 |
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
|
176 |
output(Progress.Message(Progress.Kind.warning, msg, verbose = verbose)) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
180 |
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
|
181 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
182 |
def theory(theory: Progress.Theory): Unit = output(theory.message) |
73340 | 183 |
def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} |
64909 | 184 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
185 |
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
|
186 |
body: => A, |
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
187 |
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
|
188 |
enabled: Boolean = true |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
189 |
): A = Timing.timeit(body, message = message, enabled = enabled, output = echo(_)) |
65921 | 190 |
|
77524 | 191 |
@volatile private var is_stopped = false |
73367 | 192 |
def stop(): Unit = { is_stopped = true } |
75393 | 193 |
def stopped: Boolean = { |
73367 | 194 |
if (Thread.interrupted()) is_stopped = true |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
195 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
196 |
} |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
197 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
198 |
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
|
199 |
final def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() |
61276 | 200 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 201 |
|
77506
a8175b950173
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm
parents:
77504
diff
changeset
|
202 |
final def bash(script: String, |
64201 | 203 |
cwd: JFile = null, |
73897 | 204 |
env: JMap[String, String] = Isabelle_System.settings(), |
64201 | 205 |
redirect: Boolean = false, |
65930 | 206 |
echo: Boolean = false, |
72599 | 207 |
watchdog: Time = Time.zero, |
75393 | 208 |
strict: Boolean = true |
209 |
): Process_Result = { |
|
72599 | 210 |
val result = |
211 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
212 |
progress_stdout = echo_if(echo, _), |
|
213 |
progress_stderr = echo_if(echo, _), |
|
214 |
watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)), |
|
215 |
strict = strict) |
|
216 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 217 |
} |
61276 | 218 |
} |
219 |
||
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
220 |
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
|
221 |
extends Progress { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
222 |
override def output(message: Progress.Message): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
223 |
if (do_output(message)) { |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
224 |
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
|
225 |
} |
77503 | 226 |
|
227 |
override def toString: String = super.toString + ": console" |
|
61276 | 228 |
} |
65888 | 229 |
|
77507 | 230 |
class File_Progress(path: Path, override val verbose: Boolean = false) |
231 |
extends Progress { |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
232 |
override def output(message: Progress.Message): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
233 |
if (do_output(message)) File.append(path, message.output_text + "\n") |
65888 | 234 |
|
77503 | 235 |
override def toString: String = super.toString + ": " + path.toString |
65888 | 236 |
} |
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
|
237 |
|
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
|
238 |
|
78155 | 239 |
/* database progress */ |
240 |
||
241 |
class Database_Progress( |
|
78156
da5cc332ded3
prefer Database_Progress, which is more robust (amending afb1a19307c4);
wenzelm
parents:
78155
diff
changeset
|
242 |
val db: SQL.Database, |
da5cc332ded3
prefer Database_Progress, which is more robust (amending afb1a19307c4);
wenzelm
parents:
78155
diff
changeset
|
243 |
val base_progress: Progress, |
78155 | 244 |
val hostname: String = Isabelle_System.hostname(), |
245 |
val context_uuid: String = UUID.random().toString) |
|
246 |
extends Progress { |
|
247 |
database_progress => |
|
248 |
||
249 |
private var _agent_uuid: String = "" |
|
250 |
private var _context: Long = 0 |
|
251 |
private var _seen: Long = 0 |
|
252 |
||
253 |
def agent_uuid: String = synchronized { _agent_uuid } |
|
254 |
||
255 |
private def transaction_lock[A](body: => A, create: Boolean = false): A = |
|
256 |
db.transaction_lock(Progress.Data.all_tables, create = create)(body) |
|
257 |
||
258 |
private def init(): Unit = synchronized { |
|
259 |
transaction_lock(create = true, body = { |
|
260 |
Progress.Data.read_progress_context(db, context_uuid) match { |
|
261 |
case Some(context) => |
|
262 |
_context = context |
|
263 |
_agent_uuid = UUID.random().toString |
|
264 |
case None => |
|
265 |
_context = Progress.Data.next_progress_context(db) |
|
266 |
_agent_uuid = context_uuid |
|
267 |
db.execute_statement(Progress.Data.Base.table.insert(), { stmt => |
|
268 |
stmt.string(1) = context_uuid |
|
269 |
stmt.long(2) = _context |
|
270 |
stmt.bool(3) = false |
|
271 |
}) |
|
272 |
} |
|
273 |
db.execute_statement(Progress.Data.Agents.table.insert(), { stmt => |
|
274 |
val java = ProcessHandle.current() |
|
275 |
val java_pid = java.pid |
|
276 |
val java_start = Date.instant(java.info.startInstant.get) |
|
277 |
val now = db.now() |
|
278 |
||
279 |
stmt.string(1) = _agent_uuid |
|
280 |
stmt.string(2) = context_uuid |
|
281 |
stmt.string(3) = hostname |
|
282 |
stmt.long(4) = java_pid |
|
283 |
stmt.date(5) = java_start |
|
284 |
stmt.date(6) = now |
|
285 |
stmt.date(7) = now |
|
286 |
stmt.date(8) = None |
|
287 |
stmt.long(9) = 0L |
|
288 |
}) |
|
289 |
}) |
|
290 |
if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.all_tables) |
|
291 |
} |
|
292 |
||
293 |
def exit(): Unit = synchronized { |
|
294 |
if (_context > 0) { |
|
295 |
transaction_lock { |
|
296 |
Progress.Data.update_agent(db, _agent_uuid, _seen, stop = true) |
|
297 |
} |
|
298 |
_context = 0 |
|
299 |
} |
|
300 |
} |
|
301 |
||
302 |
private def sync_database[A](body: => A): A = synchronized { |
|
303 |
require(_context > 0) |
|
304 |
transaction_lock { |
|
305 |
val stopped_db = Progress.Data.read_progress_stopped(db, _context) |
|
306 |
val stopped = base_progress.stopped |
|
307 |
||
308 |
if (stopped_db && !stopped) base_progress.stop() |
|
309 |
if (stopped && !stopped_db) Progress.Data.write_progress_stopped(db, _context, true) |
|
310 |
||
311 |
val messages = Progress.Data.read_messages(db, _context, seen = _seen) |
|
312 |
for ((seen, message) <- messages) { |
|
313 |
if (base_progress.do_output(message)) base_progress.output(message) |
|
314 |
_seen = _seen max seen |
|
315 |
} |
|
316 |
if (messages.nonEmpty) Progress.Data.update_agent(db, _agent_uuid, _seen) |
|
317 |
||
318 |
body |
|
319 |
} |
|
320 |
} |
|
321 |
||
322 |
def sync(): Unit = sync_database {} |
|
323 |
||
324 |
private def output_database(message: Progress.Message, body: => Unit): Unit = |
|
325 |
sync_database { |
|
326 |
val serial = Progress.Data.next_messages_serial(db, _context) |
|
327 |
Progress.Data.write_messages(db, _context, serial, message) |
|
328 |
||
329 |
body |
|
330 |
||
331 |
_seen = _seen max serial |
|
332 |
Progress.Data.update_agent(db, _agent_uuid, _seen) |
|
333 |
} |
|
334 |
||
335 |
override def output(message: Progress.Message): Unit = |
|
336 |
output_database(message, if (do_output(message)) base_progress.output(message)) |
|
337 |
||
338 |
override def theory(theory: Progress.Theory): Unit = |
|
339 |
output_database(theory.message, base_progress.theory(theory)) |
|
340 |
||
341 |
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = |
|
342 |
base_progress.nodes_status(nodes_status) |
|
343 |
||
344 |
override def verbose: Boolean = base_progress.verbose |
|
345 |
||
346 |
override def stop(): Unit = synchronized { base_progress.stop(); sync() } |
|
347 |
override def stopped: Boolean = sync_database { base_progress.stopped } |
|
348 |
||
349 |
override def toString: String = super.toString + ": database " + db |
|
350 |
||
351 |
init() |
|
352 |
sync() |
|
353 |
} |
|
354 |
||
355 |
||
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
|
356 |
/* 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
|
357 |
|
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
|
358 |
object Program_Progress { |
77174 | 359 |
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
|
360 |
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
|
361 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
362 |
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
|
363 |
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
|
364 |
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
|
365 |
} |
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
|
366 |
|
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
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
|
77174 | 371 |
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
|
372 |
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
|
373 |
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
|
374 |
|
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
|
375 |
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
|
376 |
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
|
377 |
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
|
378 |
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
|
379 |
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
|
380 |
} |
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
|
381 |
|
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
|
382 |
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
|
383 |
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
|
384 |
(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
|
385 |
} |
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
|
386 |
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
|
387 |
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
|
388 |
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
|
389 |
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
|
390 |
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
|
391 |
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
|
392 |
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
|
393 |
(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
|
394 |
} |
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
|
395 |
|
76997 | 396 |
(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
|
397 |
} |
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
|
398 |
} |
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
|
399 |
} |
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
|
400 |
|
77174 | 401 |
abstract class Program_Progress( |
402 |
default_heading: String = "Running", |
|
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
403 |
default_title: String = "program", |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
404 |
override val verbose: Boolean = false |
77174 | 405 |
) 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
|
406 |
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
|
407 |
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
|
408 |
|
77174 | 409 |
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
|
410 |
val programs = (_running_program.toList ::: _finished_programs).reverse |
77174 | 411 |
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
|
412 |
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
|
413 |
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
|
414 |
(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
|
415 |
} |
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
|
416 |
|
77174 | 417 |
private def start_program(heading: String, title: String): Unit = synchronized { |
418 |
_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
|
419 |
} |
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 |
|
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
|
421 |
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
|
422 |
_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
|
423 |
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
|
424 |
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
|
425 |
_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
|
426 |
_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
|
427 |
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
|
428 |
} |
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 |
} |
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 |
|
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 |
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
|
432 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77507
diff
changeset
|
433 |
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
|
434 |
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
|
435 |
detect_program(writeln_msg).map(Word.explode) match { |
77174 | 436 |
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
|
437 |
stop_program() |
77174 | 438 |
start_program(a, Word.implode(bs)) |
439 |
case _ => |
|
440 |
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
|
441 |
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
|
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 |
} |
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 |
} |