# HG changeset patch
# User wenzelm
# Date 1606407813 -3600
# Node ID caa182bdab7aa55de240af332249e7072679bdbd
# Parent  2da1993fe903b695f3e4bc7337d1997349ddc91c
clarified options: batch-build has pide_reports disabled by default (requires significant resources);

diff -r 2da1993fe903 -r caa182bdab7a NEWS
--- a/NEWS	Thu Nov 26 17:01:19 2020 +0100
+++ b/NEWS	Thu Nov 26 17:23:33 2020 +0100
@@ -242,6 +242,9 @@
 
   ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
 
+This includes full PIDE markup, if option "build_pide_reports" is
+enabled.
+
 * The command-line tool "isabelle build" provides option -P DIR to
 produce PDF/HTML presentation in the specified directory; -P: refers to
 the standard directory according to ISABELLE_BROWSER_INFO /
diff -r 2da1993fe903 -r caa182bdab7a etc/options
--- a/etc/options	Thu Nov 26 17:01:19 2020 +0100
+++ b/etc/options	Thu Nov 26 17:23:33 2020 +0100
@@ -150,6 +150,9 @@
 option pide_reports : bool = true
   -- "report PIDE markup"
 
+option build_pide_reports : bool = false
+  -- "report PIDE markup in batch build"
+
 
 section "Editor Session"
 
diff -r 2da1993fe903 -r caa182bdab7a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Nov 26 17:01:19 2020 +0100
+++ b/src/Pure/Tools/build.scala	Thu Nov 26 17:23:33 2020 +0100
@@ -202,7 +202,7 @@
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
-        "pide_reports=false"  // FIXME
+        ("pide_reports=" + options.bool("build_pide_reports"))
 
     val store = Sessions.store(build_options)