author | wenzelm |
Sat, 11 Feb 2023 20:09:37 +0100 | |
changeset 77245 | 1e2670d9dc18 |
parent 77244 | 2e5a3955bc69 |
child 77246 | 173c2fb78290 |
permissions | -rw-r--r-- |
77238 | 1 |
/* Title: Pure/Tools/build_process.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build process for sessions, with build database, optional heap, and |
|
5 |
optional presentation. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
object Build_Process { |
|
77244 | 12 |
/* static information */ |
77238 | 13 |
|
77244 | 14 |
object Session_Context { |
15 |
def empty(session: String): Session_Context = new Session_Context(session, Time.zero, Nil) |
|
77238 | 16 |
|
77239 | 17 |
def load( |
18 |
session: String, |
|
19 |
store: Sessions.Store, |
|
20 |
progress: Progress = new Progress |
|
77244 | 21 |
): Session_Context = { |
77239 | 22 |
store.try_open_database(session) match { |
23 |
case None => empty(session) |
|
77238 | 24 |
case Some(db) => |
25 |
def ignore_error(msg: String) = { |
|
26 |
progress.echo_warning("Ignoring bad database " + db + |
|
77239 | 27 |
" for session " + quote(session) + (if (msg == "") "" else ":\n" + msg)) |
28 |
empty(session) |
|
77238 | 29 |
} |
30 |
try { |
|
77239 | 31 |
val command_timings = store.read_command_timings(db, session) |
32 |
val elapsed = |
|
33 |
store.read_session_timing(db, session) match { |
|
34 |
case Markup.Elapsed(s) => Time.seconds(s) |
|
35 |
case _ => Time.zero |
|
77238 | 36 |
} |
77244 | 37 |
new Session_Context(session, elapsed, command_timings) |
77238 | 38 |
} |
39 |
catch { |
|
40 |
case ERROR(msg) => ignore_error(msg) |
|
41 |
case exn: java.lang.Error => ignore_error(Exn.message(exn)) |
|
42 |
case _: XML.Error => ignore_error("XML.Error") |
|
43 |
} |
|
44 |
finally { db.close() } |
|
45 |
} |
|
46 |
} |
|
47 |
} |
|
77239 | 48 |
|
77244 | 49 |
final class Session_Context( |
77239 | 50 |
val session: String, |
77244 | 51 |
val old_time: Time, |
52 |
val old_command_timings: List[Properties.T] |
|
77239 | 53 |
) { |
77244 | 54 |
def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty |
77240 | 55 |
|
77245
1e2670d9dc18
tuned message: old_time not sufficiently prominent nor accurate to be printed;
wenzelm
parents:
77244
diff
changeset
|
56 |
override def toString: String = session |
77239 | 57 |
} |
77238 | 58 |
} |