src/Pure/General/pretty.ML
changeset 80813 9dd4dcb08d37
parent 80812 0f820da558f9
child 80821 eb383d50564b
--- 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;