--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Nov 04 12:32:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Nov 04 12:37:45 2021 +0100
@@ -85,7 +85,7 @@
}
using(store.open_database_context())(db_context =>
{
- for (`export` <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
+ for (entry <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
val prefix = args.name.split('/') match {
case Array("mirabelle", action, "finalize") =>
s"${action} finalize "
@@ -93,7 +93,7 @@
s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset} "
case _ => ""
}
- val lines = Pretty.string_of(export.uncompressed_yxml).trim()
+ val lines = Pretty.string_of(entry.uncompressed_yxml).trim()
val body = Library.prefix_lines(prefix, lines) + "\n"
val log_file = output_dir + Path.basic("mirabelle.log")
File.append(log_file, body)
--- a/src/Pure/PIDE/session.scala Thu Nov 04 12:32:42 2021 +0100
+++ b/src/Pure/PIDE/session.scala Thu Nov 04 12:37:45 2021 +0100
@@ -507,8 +507,8 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
- val `export` = Export.make_entry("", args, msg.chunk, cache)
- change_command(_.add_export(id, (args.serial, export)))
+ val entry = Export.make_entry("", args, msg.chunk, cache)
+ change_command(_.add_export(id, (args.serial, entry)))
case Protocol.Loading_Theory(node_name, id) =>
val blobs_info = build_blobs_info(node_name)
--- a/src/Pure/Tools/build_job.scala Thu Nov 04 12:32:42 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Nov 04 12:37:45 2021 +0100
@@ -325,7 +325,7 @@
case _ => false
}
- private def `export`(msg: Prover.Protocol_Output): Boolean =
+ private def export_(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Protocol.Export(args) =>
export_consumer(session_name, args, msg.chunk)
@@ -337,7 +337,7 @@
List(
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
- Markup.EXPORT -> export,
+ Markup.EXPORT -> export_,
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
@@ -364,7 +364,7 @@
if (!progress.stopped) {
val rendering = new Rendering(snapshot, options, session)
- def `export`(name: String, xml: XML.Body, compress: Boolean = true): Unit =
+ def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit =
{
if (!progress.stopped) {
val theory_name = snapshot.node_name.theory
@@ -375,7 +375,7 @@
}
}
def export_text(name: String, text: String, compress: Boolean = true): Unit =
- export(name, List(XML.Text(text)), compress = compress)
+ export_(name, List(XML.Text(text)), compress = compress)
for (command <- snapshot.snippet_command) {
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
@@ -385,10 +385,10 @@
cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
- export(Export.MARKUP + (i + 1), xml)
+ export_(Export.MARKUP + (i + 1), xml)
}
- export(Export.MARKUP, snapshot.xml_markup())
- export(Export.MESSAGES, snapshot.messages.map(_._1))
+ 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.DOCUMENT_CITATIONS, cat_lines(citations))