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)