# HG changeset patch
# User wenzelm
# Date 1725647480 -7200
# Node ID db114ec720cbf19242b9eed9f498caa163e456e6
# Parent  84e8867925367117a4ca1154724377a3aed1f627
more thorough Protocol_Message.clean_output, following Isabelle/Scala;

diff -r 84e886792536 -r db114ec720cb src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Fri Sep 06 20:31:20 2024 +0200
@@ -200,7 +200,7 @@
     @{thm test_2.simps(1)}
     |> Thm.prop_of
     |> Syntax.string_of_term \<^context>
-    |> YXML.content_of
+    |> Protocol_Message.clean_output
   val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
 in \<^assert> (actual = expected) end
 \<close>
diff -r 84e886792536 -r db114ec720cb src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -422,7 +422,7 @@
       (*^ "\n" ^ string_of_reports reports*)
   in
     "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^
-      YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
+      Protocol_Message.clean_output (Syntax.string_of_term_global thy t) ^ "\n" ^
       space_implode "; " (map string_of_mtd_result results)
   end
 
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -143,7 +143,7 @@
 val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
 fun maybe_quote ctxt y =
   let
-    val s = YXML.content_of y
+    val s = Protocol_Message.clean_output y
     val is_literal = Keyword.is_literal (Thy_Header.get_keywords' ctxt)
     val q = if Config.get ctxt proof_cartouches then cartouche else quote
   in
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -318,7 +318,7 @@
 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
 
 fun quot_normal_name_for_type ctxt T =
-  quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T)
+  quot_normal_prefix ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T)
 
 val strip_first_name_sep =
   Substring.full #> Substring.position name_sep ##> Substring.triml 1
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -303,7 +303,7 @@
 
 fun bound_comment ctxt debug nick T R =
   short_name nick ^
-  (if debug then " :: " ^ YXML.content_of (Syntax.string_of_typ ctxt T) else "") ^
+  (if debug then " :: " ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T) else "") ^
   " : " ^ string_for_rep R
 
 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -162,7 +162,7 @@
 
     fun nth_name j =
       (case xref of
-        Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
+        Facts.Fact s => cartouche (simplify_spaces (Protocol_Message.clean_output s)) ^ bracket
       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
       | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
       | Facts.Named ((name, _), SOME intervals) =>
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -165,7 +165,7 @@
    expect : string}
 
 fun string_of_params (params : params) =
-  YXML.content_of (ML_Pretty.string_of (ML_system_pretty (params, 100)))
+  Protocol_Message.clean_output (ML_Pretty.string_of (ML_system_pretty (params, 100)))
 
 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
   induction_rules = Exclude ?
diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -132,7 +132,7 @@
 fun hackish_string_of_term ctxt =
   (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
   #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
-  #> YXML.content_of
+  #> Protocol_Message.clean_output
   #> simplify_spaces
 
 val spying_version = "d"
diff -r 84e886792536 -r db114ec720cb src/Pure/PIDE/protocol_message.ML
--- a/src/Pure/PIDE/protocol_message.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -10,6 +10,7 @@
   val marker: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
+  val clean_output: string -> string
 end;
 
 structure Protocol_Message: PROTOCOL_MESSAGE =
@@ -37,4 +38,16 @@
 fun command_positions_yxml id =
   YXML.string_of_body o command_positions id o YXML.parse_body;
 
+
+(* clean output *)
+
+fun clean_output msg =
+  (case try YXML.parse_body msg of
+    SOME xml =>
+      xml |> XML.filter_elements
+        {remove = fn a => a = Markup.reportN,
+         expose = fn a => a = Markup.no_reportN}
+      |> XML.content_of
+  | NONE => msg);
+
 end;
diff -r 84e886792536 -r db114ec720cb src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -39,6 +39,7 @@
   val enclose: string -> string -> body -> body
   val add_content: tree -> Buffer.T -> Buffer.T
   val trim_blanks: body -> body
+  val filter_elements: {remove: string -> bool, expose: string -> bool} -> body -> body
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
@@ -111,6 +112,26 @@
       | Text s => s |> raw_explode |> trim Symbol.is_blank |> implode |> string);
 
 
+(* filter markup elements *)
+
+fun filter_elements {remove, expose} =
+  let
+    fun filter ts =
+      ts |> maps (fn t =>
+        (case XML.unwrap_elem t of
+          SOME ((markup, body1), body2) =>
+            if remove (#1 markup) then []
+            else if expose (#1 markup) then filter body2
+            else [XML.wrap_elem ((markup, body1), filter body2)]
+        | NONE =>
+            (case t of
+              XML.Elem (markup, body) =>
+                if remove (#1 markup) then []
+                else if expose (#1 markup) then filter body
+                else [XML.Elem (markup, filter body)]
+            | _ => [t])));
+  in filter end;
+
 
 (** string representation **)
 
diff -r 84e886792536 -r db114ec720cb src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -33,7 +33,6 @@
   val parse_body_bytes: Bytes.T -> XML.body
   val parse: string -> XML.tree
   val parse_bytes: Bytes.T -> XML.tree
-  val content_of: string -> string
   val is_wellformed: string -> bool
 end;
 
@@ -170,8 +169,6 @@
 
 end;
 
-val content_of = parse_body #> XML.content_of;
-
 fun is_wellformed s = string_of_body (parse_body s) = s
   handle Fail _ => false;