# HG changeset patch
# User wenzelm
# Date 1728896763 -7200
# Node ID 37c039c308909bf101fd85bdf8266e22b7ed4807
# Parent  b16e6cacf739934a3b9fa84716ca6409699c6b60
tuned;

diff -r b16e6cacf739 -r 37c039c30890 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 12 22:11:38 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Oct 14 11:06:03 2024 +0200
@@ -205,6 +205,10 @@
 
 local
 
+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;
+
 val par_block = Syntax_Ext.block_indent 1;
 val par_bg = make_literal "(";
 val par_en = make_literal ")";
@@ -222,11 +226,54 @@
       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 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
 
-    fun syntax _ ([], args) = ([], args)
+    and combination p c a args =
+      (case translation p a args of
+        SOME prts => prts
+      | NONE =>
+          (*find matching table entry, or print as prefix / postfix*)
+          let
+            val nargs = length args;
+            val entry =
+              tabs |> get_first (fn tab =>
+                Symtab.lookup_list tab a |> find_first (fn (_, n, _) =>
+                  nargs = n orelse nargs > n andalso not type_mode));
+          in
+            (case entry of
+              NONE =>
+                if nargs = 0 then [Pretty.marks_str (markup a, extern a)]
+                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 translation p a args =
+      (case markup_trans a args of
+        SOME prt => SOME [prt]
+      | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE))
+
+    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 syntax _ ([], args) = ([], args)
       | syntax m (Arg p :: symbs, arg :: args) =
           let val (prts, args') = syntax m (symbs, args);
           in (main p arg @ prts, args') end
@@ -248,54 +295,7 @@
           let
             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 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 translation p a args =
-      (case markup_trans a args of
-        SOME prt => SOME [prt]
-      | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE))
-
-    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*)
-          let
-            val nargs = length args;
-            val entry =
-              tabs |> get_first (fn tab =>
-                Symtab.lookup_list tab a |> find_first (fn (_, n, _) =>
-                  nargs = n orelse nargs > n andalso not type_mode));
-          in
-            (case entry of
-              NONE =>
-                if nargs = 0 then [Pretty.marks_str (markup a, extern a)]
-                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 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 (prt :: prts, args') end;
 
   in main (Config.get ctxt pretty_priority) end;