clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;

--- a/src/Pure/General/pretty.ML	Fri Sep 06 13:49:43 2024 +0200
+++ b/src/Pure/General/pretty.ML	Fri Sep 06 13:57:06 2024 +0200
@@ -29,6 +29,7 @@
     T list -> T
   val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
   val str: string -> T
+  val dots: T
   val brk: int -> T
   val brk_indent: int -> int -> T
   val fbrk: T
@@ -148,6 +149,7 @@
 (** derived operations to create formatting expressions **)
 
 val str = T o ML_Pretty.str;
+val dots = T ML_Pretty.dots;
 
 fun brk_indent wd ind = T (ML_Pretty.PrettyBreak (short_nat wd, short_nat ind));
 fun brk wd = brk_indent wd 0;

--- a/src/Pure/ML/ml_pp.ML	Fri Sep 06 13:49:43 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML	Fri Sep 06 13:57:06 2024 +0200
@@ -79,7 +79,7 @@
 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
 fun prt_term parens (dp: FixedInt.int) t =
-  if dp <= 0 then Pretty.str "..."
+  if dp <= 0 then Pretty.dots
   else
     (case t of
       _ $ _ =>
@@ -98,7 +98,7 @@
     | Bound a => prt_app "Bound" (Pretty.from_ML (ML_system_pretty (a, dp - 1))));
 
 fun prt_proof parens dp prf =
-  if dp <= 0 then Pretty.str "..."
+  if dp <= 0 then Pretty.dots
   else
     (case prf of
       _ % _ => prt_proofs parens dp prf

--- a/src/Pure/ML/ml_pretty.ML	Fri Sep 06 13:49:43 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Fri Sep 06 13:57:06 2024 +0200
@@ -11,6 +11,7 @@
   val block: pretty list -> pretty
   val str: string -> pretty
   val brk: FixedInt.int -> pretty
+  val dots: pretty
   val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) ->
     ('a * 'b) * FixedInt.int -> pretty
   val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
@@ -34,13 +35,15 @@
 val str = PrettyString;
 fun brk width = PrettyBreak (width, 0);
 
+val dots = str "...";
+
 fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
 
 fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
   let
     fun elems _ [] = []
-      | elems 0 _ = [str "..."]
+      | elems 0 _ = [dots]
       | elems d [x] = [pretty (x, d)]
       | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
@@ -48,7 +51,7 @@
 
 (* prune *)
 
-fun prune (0: FixedInt.int) (PrettyBlock _) = str "..."
+fun prune (0: FixedInt.int) (PrettyBlock _) = dots
   | prune depth (PrettyBlock (ind, consistent, context, body)) =
       PrettyBlock (ind, consistent, context, map (prune (depth - 1)) body)
   | prune _ prt = prt;