--- 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).
--- 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"
--- 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
--- 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
}
--- 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 {
--- 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)))
}
--- 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)