src/Pure/PIDE/session.scala
changeset 74685 0ab5e35ac964
parent 74657 9fcf80ceb863
child 74731 161e84e6b40a
--- 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)