src/Pure/General/pretty.scala
changeset 49650 9fad6480300d
parent 49473 ca7e2c21b104
child 49651 c7585f8addc2
     1.1 --- a/src/Pure/General/pretty.scala	Fri Sep 28 17:06:07 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.scala	Fri Sep 28 22:53:18 2012 +0200
     1.3 @@ -66,6 +66,8 @@
     1.4  
     1.5    def standard_format(body: XML.Body): XML.Body =
     1.6      body flatMap {
     1.7 +      case XML.Wrapped_Elem(markup, body1, body2) =>
     1.8 +        List(XML.Wrapped_Elem(markup, body1, standard_format(body)))
     1.9        case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
    1.10        case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
    1.11      }
    1.12 @@ -96,6 +98,7 @@
    1.13  
    1.14      def content_length(tree: XML.Tree): Double =
    1.15        tree match {
    1.16 +        case XML.Wrapped_Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
    1.17          case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
    1.18          case XML.Text(s) => metric(s)
    1.19        }
    1.20 @@ -136,13 +139,21 @@
    1.21            else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    1.22          case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    1.23  
    1.24 +        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
    1.25 +          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
    1.26 +          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    1.27 +          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
    1.28 +          format(ts1, blockin, after, btext1)
    1.29 +
    1.30          case XML.Elem(markup, body) :: ts =>
    1.31            val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
    1.32            val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    1.33            val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
    1.34            format(ts1, blockin, after, btext1)
    1.35 +
    1.36          case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
    1.37        }
    1.38 +
    1.39      format(standard_format(input), 0.0, 0.0, Text()).content
    1.40    }
    1.41  
    1.42 @@ -160,6 +171,8 @@
    1.43          case Block(_, body) => body.flatMap(fmt)
    1.44          case Break(wd) => List(XML.Text(spaces(wd)))
    1.45          case FBreak => List(XML.Text(space))
    1.46 +        case XML.Wrapped_Elem(markup, body1, body2) =>
    1.47 +          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
    1.48          case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
    1.49          case XML.Text(_) => List(tree)
    1.50        }