clarified build options;

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

--- 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)"
 

--- 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()