# HG changeset patch
# User wenzelm
# Date 1659699287 -7200
# Node ID 2a0051496844687dd9d4d25881b3ade579ad5d1e
# Parent  f8be63d2ec6f5fe5687c4d70d5bd20a20fbbd2ef
clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;

diff -r f8be63d2ec6f -r 2a0051496844 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Aug 05 13:23:52 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Aug 05 13:34:47 2022 +0200
@@ -480,7 +480,7 @@
               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 entry = Export.make_entry("", args, msg.chunk, cache)
+                val entry = Export.make_entry(Sessions.DRAFT, args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, entry)))
 
               case Protocol.Loading_Theory(node_name, id) =>