src/Pure/General/pretty.scala
changeset 81120 080beab27264
parent 80941 fd7a70babec1
child 81121 7cacedbddba7
equal deleted inserted replaced
81119:faccef6c0806 81120:080beab27264
    19     else List(XML.Text(Symbol.spaces(n)))
    19     else List(XML.Text(Symbol.spaces(n)))
    20 
    20 
    21   val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
    21   val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
    22 
    22 
    23   def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
    23   def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
    24     XML.Elem(Markup.Block(consistent, indent), body)
    24     XML.Elem(Markup.Block(consistent = consistent, indent = indent), body)
    25 
    25 
    26   def brk(width: Int, indent: Int = 0): XML.Tree =
    26   def brk(width: Int, indent: Int = 0): XML.Tree =
    27     XML.Elem(Markup.Break(width, indent), spaces(width))
    27     XML.Elem(Markup.Break(width = width, indent = indent), spaces(width))
    28 
    28 
    29   val fbrk: XML.Tree = XML.newline
    29   val fbrk: XML.Tree = XML.newline
    30   def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
    30   def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
    31 
    31 
    32   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
    32   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)