# HG changeset patch
# User wenzelm
# Date 1728763537 -7200
# Node ID c681b1a7b78edd7b649305d21508f1fcab41b366
# Parent  06461d0d46e19aabc199f6585771d2fa9e36df2b
misc tuning and clarification;

diff -r 06461d0d46e1 -r c681b1a7b78e src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 12 21:21:50 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Oct 12 22:05:37 2024 +0200
@@ -211,7 +211,7 @@
 
 in
 
-fun pretty ctxt tabs trf markup_trans (markup, extern) ast0 =
+fun pretty ctxt tabs trf markup_trans (markup, extern) =
   let
     val type_mode = Config.get ctxt pretty_type_mode;
     val curried = Config.get ctxt pretty_curried;
@@ -222,56 +222,48 @@
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 
+    fun split_args 0 [x] ys = (x, ys)
+      | split_args 0 rev_xs ys = (Ast.Appl (rev rev_xs), ys)
+      | split_args n rev_xs (y :: ys) = split_args (n - 1) (y :: rev_xs) ys;
+
     fun syntax _ ([], args) = ([], args)
-      | syntax m (Arg p :: symbs, t :: args) =
-          let val (Ts, args') = syntax m (symbs, args);
-          in (main (t, p) @ Ts, args') end
-      | syntax m (TypArg p :: symbs, t :: args) =
-          let
-            val (Ts, args') = syntax m (symbs, args);
-          in
-            if type_mode then (main (t, p) @ Ts, args')
-            else
-              let val ctxt' = ctxt
-                |> Config.put pretty_type_mode true
-                |> Config.put pretty_priority p
-              in (pretty ctxt' tabs trf markup_trans (markup, extern) t @ Ts, args') end
-          end
+      | syntax m (Arg p :: symbs, arg :: args) =
+          let val (prts, args') = syntax m (symbs, args);
+          in (main p arg @ prts, args') end
+      | syntax m (TypArg p :: symbs, arg :: args) =
+          let val (prts, args') = syntax m (symbs, args);
+          in (main_type p arg @ prts, args') end
       | syntax m (String (literal_markup, s) :: symbs, args) =
           let
-            val (Ts, args') = syntax m (symbs, args);
-            val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
-          in (T :: Ts, args') end
+            val (prts, args') = syntax m (symbs, args);
+            val prt = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
+          in (prt :: prts, args') end
       | syntax m (Block (block, bsymbs) :: symbs, args) =
           let
-            val {markup, open_block, consistent, unbreakable, indent} = block;
-            val (bTs, args') = syntax m (bsymbs, args);
-            val (Ts, args'') = syntax m (symbs, args');
-            val prt_block =
-              {markup = markup, open_block = open_block, consistent = consistent, indent = indent};
-            val T = Pretty.markup_blocks prt_block bTs |> unbreakable ? Pretty.unbreakable;
-          in (T :: Ts, args'') end
+            val (body, args') = syntax m (bsymbs, args);
+            val (prts, args'') = syntax m (symbs, args');
+            val prt = Syntax_Ext.pretty_block block body;
+          in (prt :: prts, args'') end
       | syntax m (Break i :: symbs, args) =
           let
-            val (Ts, args') = syntax m (symbs, args);
-            val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
-          in (T :: Ts, args') end
+            val (prts, args') = syntax m (symbs, args);
+            val prt = if i < 0 then Pretty.fbrk else Pretty.brk i;
+          in (prt :: prts, args') end
 
-    and parens m (pr, args, p, p') = #1 (syntax 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 parens p q a (symbs, args) =
+      let
+        val symbs' =
+          if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
+          then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
+      in #1 (syntax (markup a) (symbs', args)) end
 
-    and split_args 0 ([x], ys) = (x, ys)
-      | split_args 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
-      | split_args n (rev_xs, y :: ys) = split_args (n - 1) (y :: rev_xs, ys)
-
-    and translation a args p =
+    and translation p a args =
       (case markup_trans a args of
         SOME prt => SOME [prt]
-      | NONE => Option.map main (SOME (trf a ctxt args, p) handle Match => NONE))
+      | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE))
 
-    and combination c a args p =
-      (case translation a args p of
+    and combination p c a args =
+      (case translation p a args of
         SOME res => res
       | NONE =>
           (*find matching table entry, or print as prefix / postfix*)
@@ -285,18 +277,27 @@
             (case entry of
               NONE =>
                 if nargs = 0 then [Pretty.marks_str (markup a, extern a)]
-                else main (application (c, args), p)
-            | SOME (pr, n, p') =>
-                if nargs = n then parens (markup a) (pr, args, p, p')
-                else main (application (split_args n ([c], args)), p))
+                else main p (application (c, args))
+            | SOME (symbs, n, q) =>
+                if nargs = n then parens p q a (symbs, args)
+                else main p (application (split_args n [c] args)))
           end)
 
-    and main (Ast.Variable x, _) = [Ast.pretty_var x]
-      | main (c as Ast.Constant a, p) = combination c a [] p
-      | main (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combination c a args p
-      | main (Ast.Appl (f :: (args as _ :: _)), p) = main (application (f, args), p)
-      | main (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
-  in main (ast0, Config.get ctxt pretty_priority) end;
+    and main _ (Ast.Variable x) = [Ast.pretty_var x]
+      | main p (c as Ast.Constant a) = combination p c a []
+      | main p (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _))) = combination p c a args
+      | main p (Ast.Appl (f :: (args as _ :: _))) = main p (application (f, args))
+      | main _ (ast as Ast.Appl _) = raise Ast.AST ("pretty: malformed ast", [ast])
+
+    and main_type p ast =
+      if type_mode then main p ast
+      else
+        (ctxt
+          |> Config.put pretty_type_mode true
+          |> Config.put pretty_priority p
+          |> pretty) tabs trf markup_trans (markup, extern) ast;
+
+  in main (Config.get ctxt pretty_priority) end;
 
 end;
 
diff -r 06461d0d46e1 -r c681b1a7b78e src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sat Oct 12 21:21:50 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sat Oct 12 22:05:37 2024 +0200
@@ -10,6 +10,7 @@
   type block =
     {markup: Markup.T list, open_block: bool, consistent: bool, unbreakable: bool, indent: int}
   val block_indent: int -> block
+  val pretty_block: block -> Pretty.T list -> Pretty.T
   datatype xsymb =
     Delim of string |
     Argument of string * int |
@@ -69,6 +70,11 @@
 fun block_indent indent : block =
   {markup = [], open_block = false, consistent = false, unbreakable = false, indent = indent};
 
+fun pretty_block {markup, open_block, consistent, indent, unbreakable} body =
+  Pretty.markup_blocks
+    {markup = markup, open_block = open_block, consistent = consistent, indent = indent} body
+  |> unbreakable ? Pretty.unbreakable;
+
 datatype xsymb =
   Delim of string |
   Argument of string * int |