# HG changeset patch
# User wenzelm
# Date 1729349674 -7200
# Node ID 785c0241d7b8f0734961862e1d8d573d8b628a94
# Parent  8927482c5639613ed146835d8fad8fed4a90c808
clarified signature;

diff -r 8927482c5639 -r 785c0241d7b8 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 19 16:45:05 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Oct 19 16:54:34 2024 +0200
@@ -36,7 +36,7 @@
   val merge_prtabs: prtabs * prtabs -> prtabs
   type pretty_ops =
    {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
-    constrain_output: Ast.ast -> Pretty.T -> Pretty.T,
+    constrain_block: Ast.ast -> Markup.output Pretty.block,
     markup_trans: string -> Ast.ast list -> Pretty.T option,
     markup: string -> Markup.T list,
     extern: string -> xstring}
@@ -227,7 +227,7 @@
 
 type pretty_ops =
  {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
-  constrain_output: Ast.ast -> Pretty.T -> Pretty.T,
+  constrain_block: Ast.ast -> Markup.output Pretty.block,
   markup_trans: string -> Ast.ast list -> Pretty.T option,
   markup: string -> Markup.T list,
   extern: string -> xstring};
@@ -300,7 +300,8 @@
           then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
         val output =
           (case constraint of
-            SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => #constrain_output ops ty
+            SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) =>
+              Pretty.make_block (#constrain_block ops ty) o single
           | _ => I);
       in #1 (syntax (#markup ops a, output) (symbs', args)) end
 
diff -r 8927482c5639 -r 785c0241d7b8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 16:45:05 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 16:54:34 2024 +0200
@@ -808,28 +808,26 @@
 
     and pretty_ast flags m =
       Printer.pretty flags ctxt prtabs
-        {trf = trf, constrain_output = make_block true, markup_trans = markup_trans,
+        {trf = trf, constrain_block = constrain_block true, markup_trans = markup_trans,
           markup = markup, extern = extern}
       #> Pretty.markup m
 
     and markup_ast is_typing a A =
-      pretty_ast (if is_typing then pretty_flags else Printer.type_mode_flags) Markup.empty a
-      |> make_block is_typing A
+      Pretty.make_block (constrain_block is_typing A)
+        [pretty_ast (if is_typing then pretty_flags else Printer.type_mode_flags) Markup.empty a]
 
-    and make_block is_typing A =
-      let
-        val cache = if is_typing then cache1 else cache2;
-        val block =
-          (case Ast.Table.lookup (! cache) A of
-            SOME block => block
-          | NONE =>
-              let
-                val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem;
-                val B = Pretty.symbolic_output (pretty_ast Printer.type_mode_flags Markup.empty A);
-                val bg = implode (bg1 :: Bytes.contents B @ [bg2]);
-                val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0};
-              in Unsynchronized.change cache (Ast.Table.update (A, block)); block end);
-      in Pretty.make_block block o single end;
+    and constrain_block is_typing A =
+      let val cache = if is_typing then cache1 else cache2 in
+        (case Ast.Table.lookup (! cache) A of
+          SOME block => block
+        | NONE =>
+            let
+              val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem;
+              val B = Pretty.symbolic_output (pretty_ast Printer.type_mode_flags Markup.empty A);
+              val bg = implode (bg1 :: Bytes.contents B @ [bg2]);
+              val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0};
+            in Unsynchronized.change cache (Ast.Table.update (A, block)); block end)
+      end;
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)