# HG changeset patch
# User wenzelm
# Date 1726089985 -7200
# Node ID 8c67b14fdd480dab15a45ef918c47e2bce73b0fc
# Parent  7c20c207af48b3f1094d0302814c6dab33ad11ca
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;

diff -r 7c20c207af48 -r 8c67b14fdd48 NEWS
--- a/NEWS	Wed Sep 11 23:07:18 2024 +0200
+++ b/NEWS	Wed Sep 11 23:26:25 2024 +0200
@@ -93,7 +93,8 @@
 
 * Pretty.pure_output_ops and Pretty.pure_string_of support
 pretty-printed output without PIDE markup. This is occasionally useful
-for special tools, in contrast to regular user output.
+for special tools, in contrast to regular user output. Manipulation of
+the print_mode via (Print_Mode.setmp []) is no longer required.
 
 * The print_mode "latex" only affects inner syntax variants, while its
 impact on Output/Markup/Pretty operations has been removed. Thus the
diff -r 7c20c207af48 -r 8c67b14fdd48 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Sep 11 23:26:25 2024 +0200
@@ -132,7 +132,7 @@
   fun check_syntax ctxt thm expected =
     let
       val obtained =
-        Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm;
+        Pretty.pure_string_of (Thm.pretty_thm (Config.put show_markup false ctxt) thm);
     in
       if obtained <> expected
       then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Sep 11 23:26:25 2024 +0200
@@ -463,8 +463,8 @@
       in Context.mapping I upd_prf ctxt end;
 
    fun string_of_typ T =
-      Print_Mode.setmp []
-        (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
+      Pretty.pure_string_of
+        (Syntax.pretty_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)) T);
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 23:26:25 2024 +0200
@@ -421,8 +421,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     fun term_to_string t =
-        Print_Mode.with_modes [""]
-          (fn () => Syntax.string_of_term ctxt t) ()
+      Pretty.pure_string_of (Syntax.pretty_term ctxt t)
     val ordered_instances =
       TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
       |> map (snd #> term_to_string)
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Sep 11 23:26:25 2024 +0200
@@ -198,8 +198,8 @@
 
 fun multiline_string_for_scope scope =
   let
-    val code_type = Print_Mode.setmp [] o Syntax.string_of_typ o Config.put show_markup false;
-    val code_term = Print_Mode.setmp [] o Syntax.string_of_term o Config.put show_markup false;
+    val code_type = Pretty.pure_string_of oo Syntax.pretty_typ o Config.put show_markup false;
+    val code_term = Pretty.pure_string_of oo Syntax.pretty_term o Config.put show_markup false;
     val (primary_cards, secondary_cards, maxes, iters, miscs) =
       quintuple_for_scope code_type code_term I scope
     val cards = primary_cards @ secondary_cards
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Sep 11 23:26:25 2024 +0200
@@ -405,7 +405,8 @@
       (s ^ (term
             |> singleton (Syntax.uncheck_terms ctxt)
             |> annotate_types_in_term ctxt
-            |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
+            |> Syntax.unparse_term ctxt
+            |> Pretty.pure_string_of
             |> simplify_spaces
             |> maybe_quote ctxt),
        ctxt |> perhaps (try (Proof_Context.augment term)))
@@ -425,7 +426,7 @@
 
     fun of_free (s, T) =
       Thy_Header.print_name' ctxt s ^ " :: " ^
-      maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
+      maybe_quote ctxt (simplify_spaces (Pretty.pure_string_of (Syntax.pretty_typ ctxt T)))
 
     fun add_frees xs (s, ctxt) =
       (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Sep 11 23:26:25 2024 +0200
@@ -131,7 +131,8 @@
 
 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)
+  #> *) Syntax.pretty_term ctxt
+  #> Pretty.pure_string_of
   #> Protocol_Message.clean_output
   #> simplify_spaces
 
diff -r 7c20c207af48 -r 8c67b14fdd48 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Wed Sep 11 23:26:25 2024 +0200
@@ -26,7 +26,8 @@
   t
   |> singleton (Syntax.uncheck_terms ctxt)
   |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
-  |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
+  |> Syntax.unparse_term ctxt
+  |> Pretty.pure_string_of
   |> Sledgehammer_Util.simplify_spaces
   |> ATP_Util.maybe_quote ctxt;