more robust reports: ensure that markup is actually present;

--- a/src/Pure/General/position.ML	Thu Sep 12 13:09:26 2024 +0200
+++ b/src/Pure/General/position.ML	Thu Sep 12 13:10:36 2024 +0200
@@ -249,16 +249,22 @@
 fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
-fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
-fun report_text pos markup txt = Output.report [reported_text pos markup txt];
+fun reported_text pos m txt =
+  if is_reported pos then Markup.markup (markup pos m) txt else "";
+
+fun report_text pos markup txt =
+  if Print_Mode.PIDE_enabled () then Output.report [reported_text pos markup txt] else ();
+
 fun report pos markup = report_text pos markup "";
 
 type report = T * Markup.T;
 type report_text = report * string;
 
-val reports_text =
-  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
-  #> Output.report;
+fun reports_text args =
+  if Print_Mode.PIDE_enabled () then
+    Output.report (args |> map (fn ((pos, m), txt) =>
+      if is_reported pos then Markup.markup (markup pos m) txt else ""))
+  else ();
 
 val reports = map (rpair "") #> reports_text;
 

--- a/src/Pure/context_position.ML	Thu Sep 12 13:09:26 2024 +0200
+++ b/src/Pure/context_position.ML	Thu Sep 12 13:10:36 2024 +0200
@@ -64,7 +64,7 @@
 
 (* PIDE reports *)
 
-fun reports_enabled0 () = Options.default_bool "pide_reports";
+fun reports_enabled0 () = Options.default_bool "pide_reports" andalso Print_Mode.PIDE_enabled ();
 fun reports_enabled_generic context = reports_enabled0 () andalso is_visible_generic context;
 val reports_enabled = reports_enabled_generic o Context.Proof;
 val reports_enabled_global = reports_enabled_generic o Context.Theory;