author | wenzelm |
Tue, 14 Mar 2023 17:05:49 +0100 | |
changeset 77652 | 5f706f7c624b |
parent 77651 | b7fe1d822dc1 |
child 78178 | a177f71dc79f |
permissions | -rw-r--r-- |
72662 | 1 |
/* Title: Pure/Tools/build_job.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build job running prover process, with rudimentary PIDE session. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import scala.collection.mutable |
|
11 |
||
12 |
||
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
13 |
trait Build_Job { |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
14 |
def cancel(): Unit = () |
77298 | 15 |
def is_finished: Boolean = false |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
16 |
def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
17 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
18 |
|
75393 | 19 |
object Build_Job { |
77396 | 20 |
/* build session */ |
21 |
||
77474 | 22 |
def start_session( |
23 |
build_context: Build_Process.Context, |
|
77505 | 24 |
progress: Progress, |
25 |
log: Logger, |
|
77474 | 26 |
session_background: Sessions.Background, |
27 |
input_shasum: SHA1.Shasum, |
|
77475 | 28 |
node_info: Host.Node_Info |
77505 | 29 |
): Session_Job = { |
77630
86ef80d13544
clarified signature: avoid confusion due to object-orientation;
wenzelm
parents:
77610
diff
changeset
|
30 |
new Session_Job(build_context, progress, log, session_background, input_shasum, node_info) |
77505 | 31 |
} |
77474 | 32 |
|
77442 | 33 |
object Session_Context { |
34 |
def load( |
|
77529
40ccee0fe19a
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents:
77521
diff
changeset
|
35 |
build_uuid: String, |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
36 |
name: String, |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
37 |
deps: List[String], |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
38 |
ancestors: List[String], |
77610
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
39 |
session_prefs: String, |
77458 | 40 |
sources_shasum: SHA1.Shasum, |
77442 | 41 |
timeout: Time, |
42 |
store: Sessions.Store, |
|
43 |
progress: Progress = new Progress |
|
44 |
): Session_Context = { |
|
77450 | 45 |
def default: Session_Context = |
77496 | 46 |
Session_Context( |
77610
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
47 |
name, deps, ancestors, session_prefs, sources_shasum, timeout, |
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
48 |
Time.zero, Bytes.empty, build_uuid) |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
49 |
|
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
50 |
store.try_open_database(name) match { |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
51 |
case None => default |
77442 | 52 |
case Some(db) => |
53 |
def ignore_error(msg: String) = { |
|
54 |
progress.echo_warning( |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
55 |
"Ignoring bad database " + db + " for session " + quote(name) + |
77442 | 56 |
if_proper(msg, ":\n" + msg)) |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
57 |
default |
77442 | 58 |
} |
59 |
try { |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
60 |
val command_timings = store.read_command_timings(db, name) |
77442 | 61 |
val elapsed = |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
62 |
store.read_session_timing(db, name) match { |
77442 | 63 |
case Markup.Elapsed(s) => Time.seconds(s) |
64 |
case _ => Time.zero |
|
65 |
} |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77442
diff
changeset
|
66 |
new Session_Context( |
77610
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
67 |
name, deps, ancestors, session_prefs, sources_shasum, timeout, |
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
68 |
elapsed, command_timings, build_uuid) |
77442 | 69 |
} |
70 |
catch { |
|
71 |
case ERROR(msg) => ignore_error(msg) |
|
72 |
case exn: java.lang.Error => ignore_error(Exn.message(exn)) |
|
73 |
case _: XML.Error => ignore_error("XML.Error") |
|
74 |
} |
|
75 |
finally { db.close() } |
|
76 |
} |
|
77 |
} |
|
78 |
} |
|
79 |
||
77496 | 80 |
sealed case class Session_Context( |
81 |
name: String, |
|
82 |
deps: List[String], |
|
83 |
ancestors: List[String], |
|
77610
3b09ae9e40cb
clarified session prefs (or "options" within the database);
wenzelm
parents:
77587
diff
changeset
|
84 |
session_prefs: String, |
77496 | 85 |
sources_shasum: SHA1.Shasum, |
86 |
timeout: Time, |
|
87 |
old_time: Time, |
|
88 |
old_command_timings_blob: Bytes, |
|
77529
40ccee0fe19a
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents:
77521
diff
changeset
|
89 |
build_uuid: String |
77652
5f706f7c624b
more thorough synchronization of internal "_state" vs. external "_database";
wenzelm
parents:
77651
diff
changeset
|
90 |
) extends Library.Named |
77442 | 91 |
|
77474 | 92 |
class Session_Job private[Build_Job]( |
77455 | 93 |
build_context: Build_Process.Context, |
77505 | 94 |
progress: Progress, |
95 |
log: Logger, |
|
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
96 |
session_background: Sessions.Background, |
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77458
diff
changeset
|
97 |
input_shasum: SHA1.Shasum, |
77649 | 98 |
node_info: Host.Node_Info |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
99 |
) extends Build_Job { |
77455 | 100 |
private val store = build_context.store |
101 |
||
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
102 |
def session_name: String = session_background.session_name |
77349
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
103 |
|
77493 | 104 |
private val info: Sessions.Info = session_background.sessions_structure(session_name) |
77550 | 105 |
private val options: Options = node_info.process_policy(info.options) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
106 |
|
77493 | 107 |
private val session_sources = |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
108 |
Sessions.Sources.load(session_background.base, cache = store.cache.compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
109 |
|
77493 | 110 |
private val store_heap = build_context.store_heap(session_name) |
77473 | 111 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
112 |
private val future_result: Future[(Process_Result, SHA1.Shasum)] = |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
113 |
Future.thread("build", uninterruptible = true) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
114 |
val env = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
115 |
Isabelle_System.settings( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
116 |
List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
117 |
|
77473 | 118 |
val session_heaps = |
119 |
session_background.info.parent match { |
|
120 |
case None => Nil |
|
121 |
case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic) |
|
122 |
} |
|
123 |
||
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77410
diff
changeset
|
124 |
val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
125 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
126 |
val eval_store = |
77463 | 127 |
if (store_heap) { |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
128 |
(if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
129 |
List("ML_Heap.save_child " + |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
130 |
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
131 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
132 |
else Nil |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
133 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
134 |
def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
135 |
session_background.base.theory_load_commands.get(node_name.theory) match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
136 |
case None => Nil |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
137 |
case Some(spans) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
138 |
val syntax = session_background.base.theory_syntax(node_name) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
139 |
val master_dir = Path.explode(node_name.master_dir) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
140 |
for (span <- spans; file <- span.loaded_files(syntax).files) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
141 |
yield { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
142 |
val src_path = Path.explode(file) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
143 |
val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
144 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
145 |
val bytes = session_sources(blob_name.node).bytes |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
146 |
val text = bytes.text |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
147 |
val chunk = Symbol.Text_Chunk(text) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
148 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
149 |
Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) -> |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
150 |
Document.Blobs.Item(bytes, text, chunk, changed = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
151 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
152 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
153 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
154 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
155 |
/* session */ |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
156 |
|
77473 | 157 |
val resources = |
77505 | 158 |
new Resources(session_background, log = log, |
77473 | 159 |
command_timings = build_context.old_command_timings(session_name)) |
160 |
||
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
161 |
val session = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
162 |
new Session(options, resources) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
163 |
override val cache: Term.Cache = store.cache |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
164 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
165 |
override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
166 |
Command.Blobs_Info.make(session_blobs(node_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
167 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
168 |
override def build_blobs(node_name: Document.Node.Name): Document.Blobs = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
169 |
Document.Blobs.make(session_blobs(node_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
170 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
171 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
172 |
object Build_Session_Errors { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
173 |
private val promise: Promise[List[String]] = Future.promise |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
174 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
175 |
def result: Exn.Result[List[String]] = promise.join_result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
176 |
def cancel(): Unit = promise.cancel() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
177 |
def apply(errs: List[String]): Unit = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
178 |
try { promise.fulfill(errs) } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
179 |
catch { case _: IllegalStateException => } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
180 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
181 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
182 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
183 |
val export_consumer = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
184 |
Export.consumer(store.open_database(session_name, output = true), store.cache, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
185 |
progress = progress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
186 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
187 |
val stdout = new StringBuilder(1000) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
188 |
val stderr = new StringBuilder(1000) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
189 |
val command_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
190 |
val theory_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
191 |
val session_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
192 |
val runtime_statistics = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
193 |
val task_statistics = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
194 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
195 |
def fun( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
196 |
name: String, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
197 |
acc: mutable.ListBuffer[Properties.T], |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
198 |
unapply: Properties.T => Option[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
199 |
): (String, Session.Protocol_Function) = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
200 |
name -> ((msg: Prover.Protocol_Output) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
201 |
unapply(msg.properties) match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
202 |
case Some(props) => acc += props; true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
203 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
204 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
205 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
206 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
207 |
session.init_protocol_handler(new Session.Protocol_Handler { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
208 |
override def exit(): Unit = Build_Session_Errors.cancel() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
209 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
210 |
private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
211 |
val (rc, errors) = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
212 |
try { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
213 |
val (rc, errs) = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
214 |
import XML.Decode._ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
215 |
pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
216 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
217 |
val errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
218 |
for (err <- errs) yield { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
219 |
val prt = Protocol_Message.expose_no_reports(err) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
220 |
Pretty.string_of(prt, metric = Symbol.Metric) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
221 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
222 |
(rc, errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
223 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
224 |
catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
225 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
226 |
session.protocol_command("Prover.stop", rc.toString) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
227 |
Build_Session_Errors(errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
228 |
true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
229 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
230 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
231 |
private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
232 |
msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
233 |
case Markup.Loading_Theory(Markup.Name(name)) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
234 |
progress.theory(Progress.Theory(name, session = session_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
235 |
false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
236 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
237 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
238 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
239 |
private def export_(msg: Prover.Protocol_Output): Boolean = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
240 |
msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
241 |
case Protocol.Export(args) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
242 |
export_consumer.make_entry(session_name, args, msg.chunk) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
243 |
true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
244 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
245 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
246 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
247 |
override val functions: Session.Protocol_Functions = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
248 |
List( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
249 |
Markup.Build_Session_Finished.name -> build_session_finished, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
250 |
Markup.Loading_Theory.name -> loading_theory, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
251 |
Markup.EXPORT -> export_, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
252 |
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
253 |
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
254 |
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
255 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
256 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
257 |
session.command_timings += Session.Consumer("command_timings") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
258 |
case Session.Command_Timing(props) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
259 |
for { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
260 |
elapsed <- Markup.Elapsed.unapply(props) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
261 |
elapsed_time = Time.seconds(elapsed) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
262 |
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
263 |
} command_timings += props.filter(Markup.command_timing_property) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
264 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
265 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
266 |
session.runtime_statistics += Session.Consumer("ML_statistics") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
267 |
case Session.Runtime_Statistics(props) => runtime_statistics += props |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
268 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
269 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
270 |
session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
271 |
case snapshot => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
272 |
if (!progress.stopped) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
273 |
def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
274 |
if (!progress.stopped) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
275 |
val theory_name = snapshot.node_name.theory |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
276 |
val args = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
277 |
Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
278 |
val body = Bytes(Symbol.encode(YXML.string_of_body(xml))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
279 |
export_consumer.make_entry(session_name, args, body) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
280 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
281 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
282 |
def export_text(name: String, text: String, compress: Boolean = true): Unit = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
283 |
export_(name, List(XML.Text(text)), compress = compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
284 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
285 |
for (command <- snapshot.snippet_command) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
286 |
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
287 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
288 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
289 |
export_text(Export.FILES, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
290 |
cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
291 |
compress = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
292 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
293 |
for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
294 |
val xml = snapshot.switch(blob_name).xml_markup() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
295 |
export_(Export.MARKUP + (i + 1), xml) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
296 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
297 |
export_(Export.MARKUP, snapshot.xml_markup()) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
298 |
export_(Export.MESSAGES, snapshot.messages.map(_._1)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
299 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
300 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
301 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
302 |
session.all_messages += Session.Consumer[Any]("build_session_output") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
303 |
case msg: Prover.Output => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
304 |
val message = msg.message |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
305 |
if (msg.is_system) resources.log(Protocol.message_text(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
306 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
307 |
if (msg.is_stdout) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
308 |
stdout ++= Symbol.encode(XML.content(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
309 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
310 |
else if (msg.is_stderr) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
311 |
stderr ++= Symbol.encode(XML.content(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
312 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
313 |
else if (msg.is_exit) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
314 |
val err = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
315 |
"Prover terminated" + |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
316 |
(msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
317 |
case Markup.Process_Result(result) => ": " + result.print_rc |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
318 |
case _ => "" |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
319 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
320 |
Build_Session_Errors(List(err)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
321 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
322 |
case _ => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
323 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
324 |
|
77455 | 325 |
build_context.session_setup(session_name, session) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
326 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
327 |
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
328 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
329 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
330 |
/* process */ |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
331 |
|
77485 | 332 |
val process = |
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77410
diff
changeset
|
333 |
Isabelle_Process.start(options, session, session_background, session_heaps, |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77410
diff
changeset
|
334 |
use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) |
77485 | 335 |
|
336 |
val timeout_request: Option[Event_Timer.Request] = |
|
337 |
if (info.timeout_ignored) None |
|
338 |
else Some(Event_Timer.request(Time.now() + info.timeout) { process.terminate() }) |
|
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
339 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
340 |
val build_errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
341 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
342 |
Exn.capture { process.await_startup() } match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
343 |
case Exn.Res(_) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
344 |
val resources_yxml = resources.init_session_yxml |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
345 |
val encode_options: XML.Encode.T[Options] = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
346 |
options => session.prover_options(options).encode |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
347 |
val args_yxml = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
348 |
YXML.string_of_body( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
349 |
{ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
350 |
import XML.Encode._ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
351 |
pair(string, list(pair(encode_options, list(pair(string, properties)))))( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
352 |
(session_name, info.theories)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
353 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
354 |
session.protocol_command("build_session", resources_yxml, args_yxml) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
355 |
Build_Session_Errors.result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
356 |
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
357 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
358 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
359 |
|
77484 | 360 |
val result0 = |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
361 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
362 |
|
77485 | 363 |
val was_timeout = |
364 |
timeout_request match { |
|
365 |
case None => false |
|
366 |
case Some(request) => !request.cancel() |
|
367 |
} |
|
368 |
||
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
369 |
session.stop() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
370 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
371 |
val export_errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
372 |
export_consumer.shutdown(close = true).map(Output.error_message_text) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
373 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
374 |
val (document_output, document_errors) = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
375 |
try { |
77484 | 376 |
if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) { |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
377 |
using(Export.open_database_context(store)) { database_context => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
378 |
val documents = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
379 |
using(database_context.open_session(session_background)) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
380 |
session_context => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
381 |
Document_Build.build_documents( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
382 |
Document_Build.context(session_context, progress = progress), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
383 |
output_sources = info.document_output, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
384 |
output_pdf = info.document_output) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
385 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
386 |
using(database_context.open_database(session_name, output = true))(session_database => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
387 |
documents.foreach(_.write(session_database.db, session_name))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
388 |
(documents.flatMap(_.log_lines), Nil) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
389 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
390 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
391 |
else (Nil, Nil) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
392 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
393 |
catch { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
394 |
case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
395 |
case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
396 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
397 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
398 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
399 |
/* process result */ |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
400 |
|
77484 | 401 |
val result1 = { |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
402 |
val theory_timing = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
403 |
theory_timings.iterator.flatMap( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
404 |
{ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
405 |
case props @ Markup.Name(name) => Some(name -> props) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
406 |
case _ => None |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
407 |
}).toMap |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
408 |
val used_theory_timings = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
409 |
for { (name, _) <- session_background.base.used_theories } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
410 |
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
411 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
412 |
val more_output = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
413 |
Library.trim_line(stdout.toString) :: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
414 |
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
415 |
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
416 |
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
417 |
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
418 |
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
419 |
document_output |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
420 |
|
77484 | 421 |
result0.output(more_output) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
422 |
.error(Library.trim_line(stderr.toString)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
423 |
.errors_rc(export_errors ::: document_errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
424 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
425 |
|
77484 | 426 |
val result2 = |
427 |
build_errors match { |
|
428 |
case Exn.Res(build_errs) => |
|
429 |
val errs = build_errs ::: document_errors |
|
430 |
if (errs.nonEmpty) { |
|
431 |
result1.error_rc.output( |
|
432 |
errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
|
433 |
errs.map(Protocol.Error_Message_Marker.apply)) |
|
434 |
} |
|
435 |
else if (progress.stopped && result1.ok) result1.copy(rc = Process_Result.RC.interrupt) |
|
436 |
else result1 |
|
437 |
case Exn.Exn(Exn.Interrupt()) => |
|
438 |
if (result1.ok) result1.copy(rc = Process_Result.RC.interrupt) |
|
439 |
else result1 |
|
440 |
case Exn.Exn(exn) => throw exn |
|
441 |
} |
|
442 |
||
77485 | 443 |
val process_result = |
444 |
if (result2.ok) result2 |
|
445 |
else if (was_timeout) result2.error(Output.error_message_text("Timeout")).timeout_rc |
|
446 |
else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt")) |
|
447 |
else result2 |
|
448 |
||
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
449 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
450 |
/* output heap */ |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
451 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
452 |
val output_shasum = |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
453 |
if (process_result.ok && store_heap && store.output_heap(session_name).is_file) { |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
454 |
SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
455 |
} |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
456 |
else SHA1.no_shasum |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
457 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
458 |
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
459 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
460 |
val build_log = |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
461 |
Build_Log.Log_File(session_name, process_result.out_lines). |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
462 |
parse_session_info( |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
463 |
command_timings = true, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
464 |
theory_timings = true, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
465 |
ml_statistics = true, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
466 |
task_statistics = true) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
467 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
468 |
// write log file |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
469 |
if (process_result.ok) { |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
470 |
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
471 |
} |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
472 |
else File.write(store.output_log(session_name), terminate_lines(log_lines)) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
473 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
474 |
// write database |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
475 |
using(store.open_database(session_name, output = true))(db => |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
476 |
store.write_session_info(db, session_name, session_sources, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
477 |
build_log = |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
478 |
if (process_result.timeout) build_log.error("Timeout") else build_log, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
479 |
build = |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
480 |
Sessions.Build_Info( |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
481 |
sources = build_context.sources_shasum(session_name), |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
482 |
input_heaps = input_shasum, |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
483 |
output_heap = output_shasum, |
77529
40ccee0fe19a
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents:
77521
diff
changeset
|
484 |
process_result.rc, |
40ccee0fe19a
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents:
77521
diff
changeset
|
485 |
build_context.build_uuid))) |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
486 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
487 |
// messages |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
488 |
process_result.err_lines.foreach(progress.echo(_)) |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
489 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
490 |
if (process_result.ok) { |
77521
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
491 |
val props = build_log.session_timing |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
492 |
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
493 |
val timing = Markup.Timing_Properties.get(props) |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
494 |
progress.echo( |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
495 |
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")", |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77509
diff
changeset
|
496 |
verbose = true) |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
497 |
progress.echo( |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
498 |
"Finished " + session_name + " (" + process_result.timing.message_resources + ")") |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
499 |
} |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
500 |
else { |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
501 |
progress.echo( |
77563 | 502 |
session_name + " FAILED (see also \"isabelle build_log -H Error " + session_name + "\")") |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
503 |
if (!process_result.interrupted) { |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
504 |
val tail = info.options.int("process_output_tail") |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
505 |
val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
506 |
val prefix = if (log_lines.length == suffix.length) Nil else List("...") |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
507 |
progress.echo(Library.trim_line(cat_lines(prefix ::: suffix))) |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
508 |
} |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
509 |
} |
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
510 |
|
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
511 |
(process_result.copy(out_lines = log_lines), output_shasum) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
512 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
513 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
514 |
override def cancel(): Unit = future_result.cancel() |
77298 | 515 |
override def is_finished: Boolean = future_result.is_finished |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77485
diff
changeset
|
516 |
override def join: (Process_Result, SHA1.Shasum) = future_result.join |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
517 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
518 |
|
77396 | 519 |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
520 |
/* theory markup/messages from session database */ |
72854 | 521 |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
522 |
def read_theory( |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
523 |
theory_context: Export.Theory_Context, |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
524 |
unicode_symbols: Boolean = false |
76205 | 525 |
): Option[Document.Snapshot] = { |
76936 | 526 |
def decode_bytes(bytes: Bytes): String = |
527 |
Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes)) |
|
528 |
||
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
529 |
def read(name: String): Export.Entry = theory_context(name, permissive = true) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
530 |
|
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
531 |
def read_xml(name: String): XML.Body = |
76936 | 532 |
YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
533 |
|
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
534 |
def read_source_file(name: String): Sessions.Source_File = |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
535 |
theory_context.session_context.source_file(name) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
536 |
|
75733 | 537 |
for { |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
538 |
id <- theory_context.document_id() |
75903 | 539 |
(thy_file, blobs_files) <- theory_context.files(permissive = true) |
75733 | 540 |
} |
541 |
yield { |
|
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
542 |
val master_dir = |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
543 |
Path.explode(Url.strip_base_name(thy_file).getOrElse( |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
544 |
error("Cannot determine theory master directory: " + quote(thy_file)))) |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
545 |
|
75733 | 546 |
val blobs = |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
547 |
blobs_files.map { name => |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
548 |
val path = Path.explode(name) |
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
549 |
val src_path = File.relative_path(master_dir, path).getOrElse(path) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
550 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
551 |
val file = read_source_file(name) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
552 |
val bytes = file.bytes |
76936 | 553 |
val text = decode_bytes(bytes) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
554 |
val chunk = Symbol.Text_Chunk(text) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
555 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
556 |
Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
557 |
Document.Blobs.Item(bytes, text, chunk, changed = false) |
75733 | 558 |
} |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
559 |
|
76936 | 560 |
val thy_source = decode_bytes(read_source_file(thy_file).bytes) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
561 |
val thy_xml = read_xml(Export.MARKUP) |
75733 | 562 |
val blobs_xml = |
563 |
for (i <- (1 to blobs.length).toList) |
|
564 |
yield read_xml(Export.MARKUP + i) |
|
72865
ebf72a3b8daa
clarified file sources: take from build database instead of file-system;
wenzelm
parents:
72864
diff
changeset
|
565 |
|
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
566 |
val markups_index = Command.Markup_Index.make(blobs.map(_._1)) |
75733 | 567 |
val markups = |
568 |
Command.Markups.make( |
|
569 |
for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) |
|
570 |
yield index -> Markup_Tree.from_XML(xml)) |
|
571 |
||
76911 | 572 |
val results = |
573 |
Command.Results.make( |
|
574 |
for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) |
|
575 |
yield i -> elem) |
|
576 |
||
76205 | 577 |
val command = |
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
578 |
Command.unparsed(thy_source, theory = true, id = id, |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
579 |
node_name = Document.Node.Name(thy_file, theory = theory_context.theory), |
76913 | 580 |
blobs_info = Command.Blobs_Info.make(blobs), |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
581 |
markups = markups, results = results) |
76205 | 582 |
|
76913 | 583 |
val doc_blobs = Document.Blobs.make(blobs) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
584 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
585 |
Document.State.init.snippet(command, doc_blobs) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
586 |
} |
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
587 |
} |
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
588 |
} |