# HG changeset patch
# User wenzelm
# Date 1592575952 -7200
# Node ID 6a64205b491a0cf2f7d29f12defd8d7d487104c1
# Parent  4320875eb8a12c77337f384e8e919a297674a95b
avoid redundant export handling for build;

diff -r 4320875eb8a1 -r 6a64205b491a etc/options
--- a/etc/options	Thu Jun 18 09:07:54 2020 +0000
+++ b/etc/options	Fri Jun 19 16:12:32 2020 +0200
@@ -153,6 +153,9 @@
 option pide_session : bool = true
   -- "build session heaps via PIDE"
 
+option pide_exports : bool = true
+  -- "store PIDE export artifacts"
+
 option pide_reports : bool = true
   -- "report PIDE markup"
 
diff -r 4320875eb8a1 -r 6a64205b491a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/Pure/PIDE/session.scala	Fri Jun 19 16:12:32 2020 +0200
@@ -501,9 +501,11 @@
 
               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.bytes, cache = xz_cache)
-                change_command(_.add_export(id, (args.serial, export)))
+                if (session_options.bool("pide_exports")) {
+                  val id = Value.Long.unapply(args.id.get).get
+                  val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                  change_command(_.add_export(id, (args.serial, export)))
+                }
 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
diff -r 4320875eb8a1 -r 6a64205b491a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/Pure/Tools/build.scala	Fri Jun 19 16:12:32 2020 +0200
@@ -492,6 +492,7 @@
         "ML_statistics" +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
+        "pide_exports=false" +
         "pide_reports=false"
 
     val store = Sessions.store(build_options)