# HG changeset patch
# User wenzelm
# Date 1726139436 -7200
# Node ID 0ed02f473cf94ceb222a674cce4c512c412cdce2
# Parent  32d0a41eea25df929212f8324a71dad53fd444a9
more robust reports: ensure that markup is actually present;

diff -r 32d0a41eea25 -r 0ed02f473cf9 src/Pure/General/position.ML
--- 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;
 
diff -r 32d0a41eea25 -r 0ed02f473cf9 src/Pure/context_position.ML
--- 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;