# HG changeset patch
# User wenzelm
# Date 1726163168 -7200
# Node ID 9af593e9e454729a3a07eaeb41a0df972b5977b7
# Parent  e71cb37c7395d2b44ea02c8910342db4419c96d9
prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;

diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Thu Sep 12 19:46:08 2024 +0200
@@ -199,8 +199,8 @@
   val actual =
     @{thm test_2.simps(1)}
     |> Thm.prop_of
-    |> Syntax.string_of_term \<^context>
-    |> Protocol_Message.clean_output
+    |> Syntax.pretty_term \<^context>
+    |> Pretty.pure_string_of
   val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
 in \<^assert> (actual = expected) end
 \<close>
diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 12 19:46:08 2024 +0200
@@ -422,7 +422,7 @@
       (*^ "\n" ^ string_of_reports reports*)
   in
     "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^
-      Protocol_Message.clean_output (Syntax.string_of_term_global thy t) ^ "\n" ^
+      Pretty.pure_string_of (Syntax.pretty_term_global thy t) ^ "\n" ^
       space_implode "; " (map string_of_mtd_result results)
   end
 
diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Sep 12 19:46:08 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 ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T)
+  quot_normal_prefix ^ Pretty.pure_string_of (Syntax.pretty_typ ctxt T)
 
 val strip_first_name_sep =
   Substring.full #> Substring.position name_sep ##> Substring.triml 1
diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 12 19:46:08 2024 +0200
@@ -303,7 +303,7 @@
 
 fun bound_comment ctxt debug nick T R =
   short_name nick ^
-  (if debug then " :: " ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T) else "") ^
+  (if debug then " :: " ^ Pretty.pure_string_of (Syntax.pretty_typ ctxt T) else "") ^
   " : " ^ string_for_rep R
 
 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Sep 12 19:46:08 2024 +0200
@@ -165,7 +165,7 @@
    expect : string}
 
 fun string_of_params (params : params) =
-  Protocol_Message.clean_output (ML_Pretty.string_of (ML_system_pretty (params, 100)))
+  Pretty.pure_string_of (Pretty.from_ML (ML_system_pretty (params, 100)))
 
 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
   induction_rules = Exclude ?
diff -r e71cb37c7395 -r 9af593e9e454 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 12 15:09:07 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 12 19:46:08 2024 +0200
@@ -133,7 +133,6 @@
   (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
   #> *) Syntax.pretty_term ctxt
   #> Pretty.pure_string_of
-  #> Protocol_Message.clean_output
   #> simplify_spaces
 
 val spying_version = "d"