# HG changeset patch
# User wenzelm
# Date 1678969105 -3600
# Node ID 488a48453d746040cb59fd185244a377f9934c20
# Parent  08fcde7c55c07ac91a2ef35377625dfd5e8b8df3
clarified build options;

diff -r 08fcde7c55c0 -r 488a48453d74 NEWS
--- a/NEWS	Thu Mar 16 11:44:07 2023 +0100
+++ b/NEWS	Thu Mar 16 13:18:25 2023 +0100
@@ -291,6 +291,9 @@
 "isabelle docker_build", to emphasize its non-relation to "isabelle
 build".
 
+* System option "build_pide_reports" has been discontinued: it coincides
+with "pide_reports".
+
 * System option "ML_process_policy" has been renamed to
 "process_policy", as it may affect other processes as well (notably in
 "isabelle build").
diff -r 08fcde7c55c0 -r 488a48453d74 etc/options
--- a/etc/options	Thu Mar 16 11:44:07 2023 +0100
+++ b/etc/options	Thu Mar 16 13:18:25 2023 +0100
@@ -50,6 +50,9 @@
 
 section "Prover Output"
 
+option pide_reports : bool = true for content
+  -- "enable reports of PIDE markup"
+
 option show_types : bool = false for content
   -- "show type constraints when printing terms"
 option show_sorts : bool = false for content
@@ -171,12 +174,6 @@
 
 section "Build Process"
 
-option pide_reports : bool = true for content
-  -- "report PIDE markup (in ML)"
-
-option build_pide_reports : bool = true for content
-  -- "report PIDE markup (in batch build)"
-
 option build_hostname : string = ""
   -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"
 
diff -r 08fcde7c55c0 -r 488a48453d74 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 16 11:44:07 2023 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 16 13:18:25 2023 +0100
@@ -70,11 +70,7 @@
     Isabelle_System.hostname(options.string("build_hostname"))
 
   def build_init(options: Options, cache: Term.Cache = Term.Cache.make()): Sessions.Store = {
-    val build_options =
-      options +
-        "completion_limit=0" +
-        "editor_tracing_messages=0" +
-        ("pide_reports=" + options.bool("build_pide_reports"))
+    val build_options = options + "completion_limit=0" + "editor_tracing_messages=0"
     val store = Sessions.store(build_options, cache = cache)
 
     Isabelle_Fonts.init()