# HG changeset patch # User wenzelm # Date 1606411926 -3600 # Node ID 178de0e275a12252e2d5fee87b3cedd6b453ad7f # Parent 35d1fc20df224532fb4b9d76644dcd4aa0da1b28# Parent 01c9b303303611c549ca64e86f8f67f690ab37a5 merged diff -r 35d1fc20df22 -r 178de0e275a1 NEWS --- a/NEWS Thu Nov 26 15:51:20 2020 +0000 +++ b/NEWS Thu Nov 26 18:32:06 2020 +0100 @@ -242,6 +242,9 @@ ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g" +This includes full PIDE markup, if option "build_pide_reports" is +enabled. + * The command-line tool "isabelle build" provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / diff -r 35d1fc20df22 -r 178de0e275a1 etc/options --- a/etc/options Thu Nov 26 15:51:20 2020 +0000 +++ b/etc/options Thu Nov 26 18:32:06 2020 +0100 @@ -150,6 +150,9 @@ option pide_reports : bool = true -- "report PIDE markup" +option build_pide_reports : bool = false + -- "report PIDE markup in batch build" + section "Editor Session" diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/PIDE/command.scala Thu Nov 26 18:32:06 2020 +0100 @@ -418,7 +418,7 @@ span: Command_Span.Span): Command = { val (source, span1) = span.compact_source - new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) + new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = @@ -430,16 +430,17 @@ id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, results: Results = Results.empty, - markup: Markup_Tree = Markup_Tree.empty): Command = + markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source - new Command(id, node_name, no_blobs, span1, source1, results, markup) + new Command(id, node_name, no_blobs, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = - unparsed(XML.content(body), id = id, results = results, markup = Markup_Tree.from_XML(body)) + unparsed(XML.content(body), id = id, results = results, + markups = Markups.init(Markup_Tree.from_XML(body))) /* perspective */ @@ -554,7 +555,7 @@ val span: Command_Span.Span, val source: String, val init_results: Command.Results, - val init_markup: Markup_Tree) + val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString @@ -669,7 +670,7 @@ /* accumulated results */ val init_state: Command.State = - Command.State(this, results = init_results, markups = Command.Markups.init(init_markup)) + Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/PIDE/document.scala Thu Nov 26 18:32:06 2020 +0100 @@ -552,7 +552,29 @@ def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] - def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body + def command_snippet(command: Command): Snapshot = + { + val node_name = command.node_name + + val nodes0 = version.nodes + val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) + val version1 = Document.Version.make(nodes1) + + val edits: List[Edit_Text] = + List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) + + val state0 = state.define_command(command) + val state1 = + state0.continue_history(Future.value(version), edits, Future.value(version1)) + .define_version(version1, state0.the_assignment(version)) + .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 + + state1.snapshot(name = node_name) + } + + def xml_markup( + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body def messages: List[(XML.Tree, Position.T)] def exports: List[Export.Entry] def exports_map: Map[String, Export.Entry] @@ -712,7 +734,8 @@ def define_command(command: Command): State = { val id = command.id - copy(commands = commands + (id -> command.init_state)) + if (commands.isDefinedAt(id)) fail + else copy(commands = commands + (id -> command.init_state)) } def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id) @@ -793,10 +816,18 @@ copy(theories = theories + (id -> command.empty_state)) } - def end_theory(theory: String): (Command.State, State) = - theories.find({ case (_, st) => st.command.node_name.theory == theory }) match { + def end_theory(theory: String): (Snapshot, State) = + theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match { case None => fail - case Some((id, st)) => (st, copy(theories = theories - id)) + case Some(st) => + val command = st.command + val node_name = command.node_name + val command1 = + Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name, + results = st.results, markups = st.markups) + val state1 = copy(theories = theories - command1.id) + val snapshot = state1.snapshot(name = node_name).command_snippet(command1) + (snapshot, state1) } def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) @@ -973,11 +1004,11 @@ range: Text.Range, elements: Markup.Elements): Markup_Tree = Command.State.merge_markup(command_states(version, command), index, range, elements) - def markup_to_XML( + def xml_markup( version: Version, node_name: Node.Name, - range: Text.Range, - elements: Markup.Elements): XML.Body = + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body = { val node = version.nodes(node_name) if (node_name.is_theory) { @@ -1097,8 +1128,10 @@ } else version.nodes.commands_loading(other_node_name).headOption - def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = - state.markup_to_XML(version, node_name, range, elements) + def xml_markup( + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body = + state.xml_markup(version, node_name, range = range, elements = elements) lazy val messages: List[(XML.Tree, Position.T)] = (for { diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/PIDE/rendering.scala Thu Nov 26 18:32:06 2020 +0100 @@ -97,8 +97,8 @@ def output_messages(results: Command.Results): List[XML.Tree] = { val (states, other) = - results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList - .partition(Protocol.is_state(_)) + results.iterator.map(_._2).filterNot(Protocol.is_result).toList + .partition(Protocol.is_state) states ::: other } @@ -296,13 +296,13 @@ Some(Completion.Language_Context.inner) }).headOption.map(_.info) - def citation(range: Text.Range): Option[Text.Info[String]] = + def citations(range: Text.Range): List[Text.Info[String]] = snapshot.select(range, Rendering.citation_elements, _ => { case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => Some(Text.Info(snapshot.convert(info_range), name)) case _ => None - }).headOption.map(_.info) + }).map(_.info) /* file-system path completion */ diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/PIDE/session.scala Thu Nov 26 18:32:06 2020 +0100 @@ -181,7 +181,7 @@ /* outlets */ - val finished_theories = new Session.Outlet[Command.State](dispatcher) + val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) @@ -511,8 +511,8 @@ case Markup.Finished_Theory(theory) => try { - val st = global_state.change_result(_.end_theory(theory)) - finished_theories.post(st) + val snapshot = global_state.change_result(_.end_theory(theory)) + finished_theories.post(snapshot) } catch { case _: Document.State.Fail => bad_output() } diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/System/process_result.scala Thu Nov 26 18:32:06 2020 +0100 @@ -53,6 +53,9 @@ def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) + def errors_rc(errs: List[String]): Process_Result = + if (errs.isEmpty) this else errors(errs).error_rc + def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Thy/bibtex.scala Thu Nov 26 18:32:06 2020 +0100 @@ -191,7 +191,7 @@ models: Map[A, B]): Option[Completion.Result] = { for { - Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret)) + Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption name1 <- Completion.clean_name(name) original <- rendering.model.get_text(r) diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Thy/export.scala Thu Nov 26 18:32:06 2020 +0100 @@ -18,6 +18,7 @@ val MARKUP = "PIDE/markup" val MESSAGES = "PIDE/messages" val DOCUMENT_PREFIX = "document/" + val CITATIONS = DOCUMENT_PREFIX + "citations" val THEORY_PREFIX: String = "theory/" val PROOFS_PREFIX: String = "proofs/" diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Thy/presentation.scala Thu Nov 26 18:32:06 2020 +0100 @@ -266,7 +266,7 @@ val documents = for { doc <- info.document_variants - document <- db_context.read_document(session, doc.name) + document <- db_context.input_database(session)(read_document(_, _, doc.name)) } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc } val links = @@ -437,7 +437,7 @@ } def pide_document(snapshot: Document.Snapshot): XML.Body = - make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) + make_html(snapshot.xml_markup(elements = document_elements)) @@ -533,7 +533,7 @@ val old_document = for { - old_doc <- db_context.read_document(session, doc.name) + old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) if old_doc.sources == sources } yield { diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Thy/sessions.scala Thu Nov 26 18:32:06 2020 +0100 @@ -1190,6 +1190,22 @@ def close { database_server.foreach(_.close) } + def output_database[A](session: String)(f: SQL.Database => A): A = + database_server match { + case Some(db) => f(db) + case None => using(store.open_database(session, output = true))(f) + } + + def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] = + database_server match { + case Some(db) => f(db, session) + case None => + store.try_open_database(session) match { + case Some(db) => using(db)(f(_, session)) + case None => None + } + } + def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] = { val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view @@ -1211,16 +1227,6 @@ read_export(session, theory_name, name) getOrElse Export.empty_entry(session, theory_name, name) - def read_document(session_name: String, name: String): Option[Presentation.Document_Output] = - database_server match { - case Some(db) => Presentation.read_document(db, session_name, name) - case None => - store.try_open_database(session_name) match { - case Some(db) => using(db)(Presentation.read_document(_, session_name, name)) - case None => None - } - } - override def toString: String = { val s = diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Tools/build.scala Thu Nov 26 18:32:06 2020 +0100 @@ -202,7 +202,7 @@ options + "completion_limit=0" + "editor_tracing_messages=0" + - "pide_reports=false" // FIXME + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options) diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Tools/build_job.scala Thu Nov 26 18:32:06 2020 +0100 @@ -51,6 +51,10 @@ override val xml_cache: XML.Cache = store.xml_cache override val xz_cache: XZ.Cache = store.xz_cache } + def make_rendering(snapshot: Document.Snapshot): Rendering = + new Rendering(snapshot, options, session) { + override def model: Document.Model = ??? + } object Build_Session_Errors { @@ -157,16 +161,26 @@ case Session.Runtime_Statistics(props) => runtime_statistics += props } - session.finished_theories += Session.Consumer[Command.State]("finished_theories") + session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { - case st => - val command = st.command - val theory_name = command.node_name.theory - val args = Protocol.Export.Args(theory_name = theory_name, name = Export.MARKUP) - val xml = - st.markups(Command.Markup_Index.markup) - .to_XML(command.range, command.source, Markup.Elements.full) - export_consumer(session_name, args, Bytes(YXML.string_of_body(xml))) + case snapshot => + val rendering = make_rendering(snapshot) + + def export(name: String, xml: XML.Body) + { + val theory_name = snapshot.node_name.theory + val args = Protocol.Export.Args(theory_name = theory_name, name = name) + val bytes = Bytes(YXML.string_of_body(xml)) + if (!bytes.is_empty) export_consumer(session_name, args, bytes) + } + def export_text(name: String, text: String): Unit = + export(name, List(XML.Text(text))) + + export(Export.MARKUP, snapshot.xml_markup()) + export(Export.MESSAGES, snapshot.messages.map(_._1)) + + val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) + export_text(Export.CITATIONS, cat_lines(citations)) } session.all_messages += Session.Consumer[Any]("build_session_output") @@ -232,16 +246,18 @@ try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { - val documents = - using(store.open_database_context(deps.sessions_structure))(db_context => - Presentation.build_documents(session_name, deps, db_context, - output_sources = info.document_output, - output_pdf = info.document_output, - progress = progress, - verbose = verbose)) - using(store.open_database(session_name, output = true))(db => - documents.foreach(_.write(db, session_name))) - (documents.flatMap(_.log_lines), Nil) + using(store.open_database_context(deps.sessions_structure))(db_context => + { + val documents = + Presentation.build_documents(session_name, deps, db_context, + output_sources = info.document_output, + output_pdf = info.document_output, + progress = progress, + verbose = verbose) + db_context.output_database(session_name)(db => + documents.foreach(_.write(db, session_name))) + (documents.flatMap(_.log_lines), Nil) + }) } (Nil, Nil) } @@ -260,10 +276,9 @@ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: document_output - val more_errors = - Library.trim_line(stderr.toString) :: export_errors ::: document_errors - - process_result.output(more_output).errors(more_errors) + process_result.output(more_output) + .error(Library.trim_line(stderr.toString)) + .errors_rc(export_errors ::: document_errors) } build_errors match { diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Tools/dump.scala Thu Nov 26 18:32:06 2020 +0100 @@ -48,29 +48,22 @@ val known_aspects: List[Aspect] = List( Aspect("markup", "PIDE markup (YXML format)", - { case args => - args.write(Path.explode(Export.MARKUP), - args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) - }), + args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())), Aspect("messages", "output messages (YXML format)", - { case args => - args.write(Path.explode(Export.MESSAGES), - args.snapshot.messages.iterator.map(_._1).toList) - }), + args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))), Aspect("latex", "generated LaTeX source", - { case args => - for { - entry <- args.snapshot.exports - if entry.name_has_prefix(Export.DOCUMENT_PREFIX) - } args.write(Path.explode(entry.name), entry.uncompressed()) - }), + args => + for { + entry <- args.snapshot.exports + if entry.name_has_prefix(Export.DOCUMENT_PREFIX) + } args.write(Path.explode(entry.name), entry.uncompressed())), Aspect("theory", "foundational theory content", - { case args => - for { - entry <- args.snapshot.exports - if entry.name_has_prefix(Export.THEORY_PREFIX) - } args.write(Path.explode(entry.name), entry.uncompressed()) - }, options = List("export_theory")) + args => + for { + entry <- args.snapshot.exports + if entry.name_has_prefix(Export.THEORY_PREFIX) + } args.write(Path.explode(entry.name), entry.uncompressed()), + options = List("export_theory")) ).sortBy(_.name) def show_aspects: String = diff -r 35d1fc20df22 -r 178de0e275a1 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Pure/Tools/update.scala Thu Nov 26 18:32:06 2020 +0100 @@ -45,8 +45,8 @@ val snapshot = args.snapshot for ((node_name, node) <- snapshot.nodes) { val xml = - snapshot.state.markup_to_XML(snapshot.version, node_name, - Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) + snapshot.state.xml_markup(snapshot.version, node_name, + elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) val source1 = Symbol.encode(XML.content(update_xml(xml))) if (source1 != Symbol.encode(node.source)) { diff -r 35d1fc20df22 -r 178de0e275a1 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 18:32:06 2020 +0100 @@ -21,9 +21,21 @@ object JEdit_Rendering { + /* make rendering */ + def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) + def text(snapshot: Document.Snapshot, formatted_body: XML.Body, + results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) = + { + val command = Command.rich_text(Document_ID.make(), results, formatted_body) + val snippet = snapshot.command_snippet(command) + val model = File_Model.empty(PIDE.session) + val rendering = apply(snippet, model, PIDE.options.value) + (command.source, rendering) + } + /* popup window bounds */ diff -r 35d1fc20df22 -r 178de0e275a1 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 15:51:20 2020 +0000 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 18:32:06 2020 +0100 @@ -27,42 +27,6 @@ import org.gjt.sp.util.{SyntaxUtilities, Log} -object Pretty_Text_Area -{ - /* auxiliary */ - - private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results, - formatted_body: XML.Body): (String, Document.State) = - { - val command = Command.rich_text(Document_ID.make(), base_results, formatted_body) - val node_name = command.node_name - val edits: List[Document.Edit_Text] = - List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) - - val state0 = base_snapshot.state.define_command(command) - val version0 = base_snapshot.version - val nodes0 = version0.nodes - - val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) - val version1 = Document.Version.make(nodes1) - val state1 = - state0.continue_history(Future.value(version0), edits, Future.value(version1)) - .define_version(version1, state0.the_assignment(version0)) - .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 - - (command.source, state1) - } - - private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results, - formatted_body: XML.Body): (String, JEdit_Rendering) = - { - val (text, state) = document_state(base_snapshot, base_results, formatted_body) - val model = File_Model.empty(PIDE.session) - val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value) - (text, rendering) - } -} - class Pretty_Text_Area( view: View, close_action: () => Unit = () => (), @@ -77,7 +41,7 @@ private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty private var current_rendering: JEdit_Rendering = - Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 + JEdit_Rendering.text(current_base_snapshot, Nil)._2 private var future_refresh: Option[Future[Unit]] = None private val rich_text_area = @@ -112,7 +76,7 @@ getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor")) getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor")) - get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) + get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor")) getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor")) getGutter.setFont(jEdit.getFontProperty("view.gutter.font")) @@ -127,15 +91,15 @@ val metric = JEdit_Lib.pretty_metric(getPainter) val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0 - val base_snapshot = current_base_snapshot - val base_results = current_base_results + val snapshot = current_base_snapshot + val results = current_base_results val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) - future_refresh.map(_.cancel) + future_refresh.foreach(_.cancel) future_refresh = Some(Future.fork { val (text, rendering) = - try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) } + try { JEdit_Rendering.text(snapshot, formatted_body, results = results) } catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } Exn.Interrupt.expose()