removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);
--- a/etc/options Fri Jun 19 20:15:00 2020 +0200
+++ b/etc/options Sat Jun 20 11:01:57 2020 +0200
@@ -153,9 +153,6 @@
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/Pure/PIDE/session.scala Fri Jun 19 20:15:00 2020 +0200
+++ b/src/Pure/PIDE/session.scala Sat Jun 20 11:01:57 2020 +0200
@@ -501,11 +501,9 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
- 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)))
- }
+ 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/Tools/build.scala Fri Jun 19 20:15:00 2020 +0200
+++ b/src/Pure/Tools/build.scala Sat Jun 20 11:01:57 2020 +0200
@@ -492,7 +492,6 @@
"ML_statistics" +
"completion_limit=0" +
"editor_tracing_messages=0" +
- "pide_exports=false" +
"pide_reports=false"
val store = Sessions.store(build_options)