195 |
195 |
196 private val future_result: Future[Process_Result] = |
196 private val future_result: Future[Process_Result] = |
197 Future.thread("build") { |
197 Future.thread("build") { |
198 val parent = info.parent.getOrElse("") |
198 val parent = info.parent.getOrElse("") |
199 |
199 |
|
200 val known_theories = |
|
201 for ((theory, node_name) <- deps(name).known_theories.toList) |
|
202 yield (theory, node_name.node) |
|
203 |
200 val args_yxml = |
204 val args_yxml = |
201 YXML.string_of_body( |
205 YXML.string_of_body( |
202 { |
206 { |
203 import XML.Encode._ |
207 import XML.Encode._ |
204 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, |
208 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, |
205 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, |
209 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, |
206 pair(string, pair(string, pair(string, pair(Path.encode, |
210 pair(string, pair(string, pair(string, pair(Path.encode, |
207 list(pair(Options.encode, list(string))))))))))))))( |
211 pair(list(pair(Options.encode, list(string))), |
|
212 list(pair(string, string))))))))))))))( |
208 (Symbol.codes, (command_timings, (do_output, (verbose, |
213 (Symbol.codes, (command_timings, (do_output, (verbose, |
209 (store.browser_info, (info.document_files, (File.standard_path(graph_file), |
214 (store.browser_info, (info.document_files, (File.standard_path(graph_file), |
210 (parent, (info.chapter, (name, (Path.current, |
215 (parent, (info.chapter, (name, (Path.current, |
211 info.theories)))))))))))) |
216 (info.theories, |
|
217 known_theories))))))))))))) |
212 }) |
218 }) |
213 |
219 |
214 val env = |
220 val env = |
215 Isabelle_System.settings() + |
221 Isabelle_System.settings() + |
216 ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) |
222 ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) |