# HG changeset patch
# User wenzelm
# Date 1724339552 -7200
# Node ID ec1023a5c54ccb74ace593b83484be333547d913
# Parent  dad0cefb48dd7aa63627c43d42869851410e7ae4
tuned: prefer configuration options via context;

diff -r dad0cefb48dd -r ec1023a5c54c src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Thu Aug 22 16:04:06 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu Aug 22 17:12:32 2024 +0200
@@ -202,10 +202,14 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
+val pretty_type_mode = Config.declare_bool ("Syntax.pretty_type_mode", \<^here>) (K false);
+val pretty_curried = Config.declare_bool ("Syntax.pretty_curried", \<^here>) (K false);
 val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
 
-fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
+fun pretty ctxt tabs trf markup_trans markup_extern ast0 =
   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;
 
     (*default applications: prefix / postfix*)
@@ -224,8 +228,10 @@
           in
             if type_mode then (astT (t, p) @ Ts, args')
             else
-              (pretty true curried (Config.put pretty_priority p ctxt)
-                tabs trf markup_trans markup_extern t @ Ts, args')
+              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
       | synT m (String (do_mark, s) :: symbs, args) =
           let
@@ -292,13 +298,19 @@
 (* pretty_term_ast *)
 
 fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast =
-  pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
+  let val ctxt' = ctxt
+    |> Config.put pretty_type_mode false
+    |> Config.put pretty_curried curried
+  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast end;
 
 
 (* pretty_typ_ast *)
 
 fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast =
-  pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
+  let val ctxt' = ctxt
+    |> Config.put pretty_type_mode true
+    |> Config.put pretty_curried false
+  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast end;
 
 end;