# HG changeset patch
# User wenzelm
# Date 1636025865 -3600
# Node ID 0ab5e35ac964ef4fef8cb691e20847b49c78aa87
# Parent  df1b9f63b2bee25b4bf703739f24cbb61255fafa
avoid conflict with future keyword;

diff -r df1b9f63b2be -r 0ab5e35ac964 src/HOL/Tools/Mirabelle/mirabelle.scala
--- 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)
diff -r df1b9f63b2be -r 0ab5e35ac964 src/Pure/PIDE/session.scala
--- 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)
diff -r df1b9f63b2be -r 0ab5e35ac964 src/Pure/Tools/build_job.scala
--- 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))