# HG changeset patch
# User wenzelm
# Date 1592585076 -7200
# Node ID 235173749448f3700ad3447026d63c47134ee366
# Parent  ee2c7f0dd1bef01a79acbaa19c4bd8eec41edf96# Parent  3e7d89d9912efa65db1af9689b9c8b797cf73712
merged

diff -r ee2c7f0dd1be -r 235173749448 NEWS
--- a/NEWS	Fri Jun 19 09:46:47 2020 +0000
+++ b/NEWS	Fri Jun 19 18:44:36 2020 +0200
@@ -91,10 +91,6 @@
 
 *** System ***
 
-* System option "pide_session" is enabled by default, notably for
-standard "isabelle build": this allows to invoke Isabelle/Scala
-operations from Isabelle/ML.
-
 * The command-line tool "isabelle console" now supports interrupts
 properly (on Linux and macOS).
 
diff -r ee2c7f0dd1be -r 235173749448 etc/options
--- a/etc/options	Fri Jun 19 09:46:47 2020 +0000
+++ b/etc/options	Fri Jun 19 18:44:36 2020 +0200
@@ -150,9 +150,12 @@
 
 section "PIDE Build"
 
-option pide_session : bool = true
+option pide_session : bool = false
   -- "build session heaps via PIDE"
 
+option pide_exports : bool = true
+  -- "store PIDE export artifacts"
+
 option pide_reports : bool = true
   -- "report PIDE markup"
 
diff -r ee2c7f0dd1be -r 235173749448 src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Jun 19 09:46:47 2020 +0000
+++ b/src/Doc/ROOT	Fri Jun 19 18:44:36 2020 +0200
@@ -378,7 +378,7 @@
     "root.tex"
 
 session System (doc) in "System" = Pure +
-  options [document_variants = "system", thy_output_source]
+  options [document_variants = "system", thy_output_source, pide_session]
   sessions
     "HOL-Library"
   theories
diff -r ee2c7f0dd1be -r 235173749448 src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Fri Jun 19 09:46:47 2020 +0000
+++ b/src/Pure/General/xz.scala	Fri Jun 19 18:44:36 2020 +0200
@@ -28,6 +28,7 @@
 
   type Cache = ArrayCache
 
+  def no_cache(): ArrayCache = ArrayCache.getDummyCache()
   def cache(): ArrayCache = ArrayCache.getDefaultCache()
   def make_cache(): ArrayCache = new BasicArrayCache
 }
diff -r ee2c7f0dd1be -r 235173749448 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 19 09:46:47 2020 +0000
+++ b/src/Pure/PIDE/session.scala	Fri Jun 19 18:44:36 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 ee2c7f0dd1be -r 235173749448 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jun 19 09:46:47 2020 +0000
+++ b/src/Pure/Thy/export.scala	Fri Jun 19 18:44:36 2020 +0200
@@ -143,19 +143,11 @@
       regex.pattern.matcher(compound_name(theory_name, name)).matches
   }
 
-  private lazy val later: Consumer_Thread[() => Unit] =
-    Consumer_Thread.fork(name = "Export.later", daemon = true)(
-      consume = (run: () => Unit) => { run(); true })
-
   def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes,
     cache: XZ.Cache = XZ.cache()): Entry =
   {
     Entry(session_name, args.theory_name, args.name, args.executable,
-      if (args.compress) {
-        val result = Future.promise[(Boolean, Bytes)]
-        later.send(() => result.fulfill(body.maybe_compress(cache = cache)))
-        result
-      }
+      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
       else Future.value((false, body)))
   }
 
diff -r ee2c7f0dd1be -r 235173749448 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jun 19 09:46:47 2020 +0000
+++ b/src/Pure/Tools/build.scala	Fri Jun 19 18:44:36 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)