src/Pure/General/pretty.scala
changeset 61862 e2a9e46ac0fb
parent 55551 4a5f65df29fa
child 61864 3a5992c3410c
equal deleted inserted replaced
61855:32a530a5c54c 61862:e2a9e46ac0fb
    54       }
    54       }
    55   }
    55   }
    56 
    56 
    57   object Break
    57   object Break
    58   {
    58   {
    59     def apply(w: Int): XML.Tree =
    59     def apply(w: Int, i: Int = 0): XML.Tree =
    60       XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
    60       XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w))))
    61 
    61 
    62     def unapply(tree: XML.Tree): Option[Int] =
    62     def unapply(tree: XML.Tree): Option[(Int, Int)] =
    63       tree match {
    63       tree match {
    64         case XML.Elem(Markup.Break(w), _) => Some(w)
    64         case XML.Elem(Markup.Break(w, i), _) => Some((w, i))
    65         case _ => None
    65         case _ => None
    66       }
    66       }
    67   }
    67   }
    68 
    68 
    69   val FBreak = XML.Text("\n")
    69   val FBreak = XML.Text("\n")
   109     def content_length(tree: XML.Tree): Double =
   109     def content_length(tree: XML.Tree): Double =
   110       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
   110       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
   111 
   111 
   112     def breakdist(trees: XML.Body, after: Double): Double =
   112     def breakdist(trees: XML.Body, after: Double): Double =
   113       trees match {
   113       trees match {
   114         case Break(_) :: _ => 0.0
   114         case Break(_, _) :: _ => 0.0
   115         case FBreak :: _ => 0.0
   115         case FBreak :: _ => 0.0
   116         case t :: ts => content_length(t) + breakdist(ts, after)
   116         case t :: ts => content_length(t) + breakdist(ts, after)
   117         case Nil => after
   117         case Nil => after
   118       }
   118       }
   119 
   119 
   120     def forcenext(trees: XML.Body): XML.Body =
   120     def forcenext(trees: XML.Body): XML.Body =
   121       trees match {
   121       trees match {
   122         case Nil => Nil
   122         case Nil => Nil
   123         case FBreak :: _ => trees
   123         case FBreak :: _ => trees
   124         case Break(_) :: ts => FBreak :: ts
   124         case Break(_, _) :: ts => FBreak :: ts
   125         case t :: ts => t :: forcenext(ts)
   125         case t :: ts => t :: forcenext(ts)
   126       }
   126       }
   127 
   127 
   128     def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
   128     def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
   129       trees match {
   129       trees match {
   137             else pos2
   137             else pos2
   138           val btext = format(body, blockin1, breakdist(ts, after), text)
   138           val btext = format(body, blockin1, breakdist(ts, after), text)
   139           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   139           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   140           format(ts1, blockin, after, btext)
   140           format(ts1, blockin, after, btext)
   141 
   141 
   142         case Break(wd) :: ts =>
   142         case Break(wd, ind) :: ts =>
   143           if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
   143           if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
   144             format(ts, blockin, after, text.blanks(wd))
   144             format(ts, blockin, after, text.blanks(wd))
   145           else format(ts, blockin, after, text.newline.blanks(blockin))
   145           else format(ts, blockin, after, text.newline.blanks(blockin + ind))
   146         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
   146         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
   147 
   147 
   148         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
   148         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
   149           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
   149           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
   150           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   150           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   173   def unformatted(input: XML.Body): XML.Body =
   173   def unformatted(input: XML.Body): XML.Body =
   174   {
   174   {
   175     def fmt(tree: XML.Tree): XML.Body =
   175     def fmt(tree: XML.Tree): XML.Body =
   176       tree match {
   176       tree match {
   177         case Block(_, body) => body.flatMap(fmt)
   177         case Block(_, body) => body.flatMap(fmt)
   178         case Break(wd) => List(XML.Text(spaces(wd)))
   178         case Break(wd, _) => List(XML.Text(spaces(wd)))
   179         case FBreak => List(XML.Text(space))
   179         case FBreak => List(XML.Text(space))
   180         case XML.Wrapped_Elem(markup, body1, body2) =>
   180         case XML.Wrapped_Elem(markup, body1, body2) =>
   181           List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
   181           List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
   182         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
   182         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
   183         case XML.Text(_) => List(tree)
   183         case XML.Text(_) => List(tree)