# HG changeset patch
# User wenzelm
# Date 1727263804 -7200
# Node ID 7f028e2ca7db247cf758eba52102d052d25b115d
# Parent  47eb251187d6dd9e4e1ced69baf8436fc0dc8262
minor performance tuning: prefer static values;

diff -r 47eb251187d6 -r 7f028e2ca7db src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Sep 25 13:20:36 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Sep 25 13:30:04 2024 +0200
@@ -137,11 +137,11 @@
   (if s = "type" then TypArg else Arg)
   (if Lexicon.is_terminal s then 1000 else p);
 
+in
+
 fun make_string s = String ([], s);
 fun make_literal s = String (Lexicon.literal_markup s, s);
 
-in
-
 fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
   | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
       let
@@ -209,6 +209,14 @@
 val pretty_curried = Config.declare_bool ("Syntax.pretty_curried", \<^here>) (K false);
 val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
 
+local
+
+val par_block = Syntax_Ext.block_indent 1;
+val par_bg = make_string "(";
+val par_en = make_string ")";
+
+in
+
 fun pretty ctxt tabs trf markup_trans markup_extern ast0 =
   let
     val type_mode = Config.get ctxt pretty_type_mode;
@@ -255,10 +263,9 @@
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
           in (T :: Ts, args') end
 
-    and parT m (pr, args, p, p': int) = #1 (synT m
-          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
-            [Block (Syntax_Ext.block_indent 1, String ([], "(") :: pr @ [String ([], ")")])]
-           else pr, args))
+    and parT m (pr, args, p, p') = #1 (synT m
+          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
+           then [Block (par_block, par_bg :: pr @ [par_en])] else pr, args))
 
     and atomT a = Pretty.marks_str (#1 markup_extern a, #2 markup_extern a)
 
@@ -294,6 +301,8 @@
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
   in astT (ast0, Config.get ctxt pretty_priority) end;
 
+end;
+
 
 (* pretty_term_ast *)