# HG changeset patch
# User wenzelm
# Date 1709982368 -3600
# Node ID 487137973a8dbdab1a9bf4463cbfaddb4efa5237
# Parent  cf9becb6403fcde66dfe6f5c800cc2fd0b7a3956
upgrade pretty_maybe_quote following 2746dfc9ceae;

diff -r cf9becb6403f -r 487137973a8d src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 09 11:51:52 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Mar 09 12:06:08 2024 +0100
@@ -278,8 +278,11 @@
 val indent_size = 2
 
 fun pretty_maybe_quote ctxt pretty =
-  let val s = Pretty.unformatted_string_of pretty
-  in if ATP_Util.maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
+  let val s = Pretty.unformatted_string_of pretty in
+    if ATP_Util.maybe_quote ctxt s = s then pretty
+    else if Config.get ctxt ATP_Util.proof_cartouches then Pretty.cartouche pretty
+    else Pretty.quote pretty
+  end
 
 val hashw = ATP_Util.hashw
 val hashw_string = ATP_Util.hashw_string