# HG changeset patch
# User wenzelm
# Date 1729107665 -7200
# Node ID 137ea3d464be27201602a1944bc0246073f86674
# Parent  c0522b2d3df6ce68bf0066ad57f588189053abfb
clarified signature (again, reverting ec1023a5c54c);

diff -r c0522b2d3df6 -r 137ea3d464be src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Oct 16 21:22:37 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Oct 16 21:41:05 2024 +0200
@@ -33,16 +33,12 @@
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs * prtabs -> prtabs
-  val pretty_term_ast: bool -> Proof.context -> prtab list ->
+  val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> Ast.ast list -> Pretty.T option) ->
     ((string -> Markup.T list) * (string -> string)) ->
     Ast.ast -> Pretty.T list
-  val pretty_typ_ast: Proof.context -> prtab list ->
-    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (string -> Ast.ast list -> Pretty.T option) ->
-    ((string -> Markup.T list) * (string -> string)) ->
-    Ast.ast -> Pretty.T list
+  val type_mode_flags: {type_mode: bool, curried: bool}
 end;
 
 structure Printer: PRINTER =
@@ -225,10 +221,10 @@
 
 in
 
-fun pretty ctxt prtabs trf markup_trans (markup, extern) =
+val type_mode_flags = {type_mode = true, curried = false};
+
+fun pretty {type_mode, curried} ctxt prtabs trf markup_trans (markup, extern) =
   let
-    val type_mode = Config.get ctxt pretty_type_mode;
-    val curried = Config.get ctxt pretty_curried;
     val show_brackets = Config.get ctxt show_brackets;
 
     val application =
@@ -257,10 +253,8 @@
     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) prtabs trf markup_trans (markup, extern) ast
+        pretty type_mode_flags (Config.put pretty_priority p ctxt)
+          prtabs trf markup_trans (markup, extern) ast
 
     and combination p c a args constraint =
       (case translation p a args of
@@ -323,24 +317,6 @@
 
 end;
 
-
-(* pretty_term_ast *)
-
-fun pretty_term_ast curried ctxt prtabs trf markup_trans markup_extern ast =
-  let val ctxt' = ctxt
-    |> Config.put pretty_type_mode false
-    |> Config.put pretty_curried curried
-  in pretty ctxt' prtabs trf markup_trans markup_extern ast end;
-
-
-(* pretty_typ_ast *)
-
-fun pretty_typ_ast ctxt prtabs trf markup_trans markup_extern ast =
-  let val ctxt' = ctxt
-    |> Config.put pretty_type_mode true
-    |> Config.put pretty_curried false
-  in pretty ctxt' prtabs trf markup_trans markup_extern ast end;
-
 end;
 
 structure Basic_Printer: BASIC_PRINTER = Printer;
diff -r c0522b2d3df6 -r 137ea3d464be src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Oct 16 21:22:37 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Oct 16 21:41:05 2024 +0200
@@ -762,6 +762,8 @@
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
+val pretty_type_mode = Printer.pretty Printer.type_mode_flags;
+
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
     val show_markup = Config.get ctxt show_markup;
@@ -804,7 +806,7 @@
       then SOME (markup_ast false ty s) else NONE
 
     and pretty_typ_ast m ast = ast
-      |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
+      |> pretty_type_mode ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m
 
     and pretty_ast m ast = ast
@@ -835,14 +837,14 @@
 
 in
 
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
+val unparse_sort = unparse_t sort_to_ast pretty_type_mode (Markup.language_sort false);
+val unparse_typ = unparse_t typ_to_ast pretty_type_mode (Markup.language_type false);
 
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val curried = not (Pure_Thy.old_appl_syntax thy);
-  in unparse_t term_to_ast (Printer.pretty_term_ast curried) (Markup.language_term false) ctxt end;
+    val term_mode = {type_mode = false, curried = not (Pure_Thy.old_appl_syntax thy)};
+  in unparse_t term_to_ast (Printer.pretty term_mode) (Markup.language_term false) ctxt end;
 
 end;