tuned;
authorwenzelm
Sun Dec 20 12:48:56 2015 +0100 (2015-12-20)
changeset 61874a942e237c9e8
parent 61873 7e8f4df04d5d
child 61875 5348b76aa94c
tuned;
src/Pure/General/pretty.scala
     1.1 --- a/src/Pure/General/pretty.scala	Sat Dec 19 23:25:23 2015 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Sun Dec 20 12:48:56 2015 +0100
     1.3 @@ -11,8 +11,11 @@
     1.4  {
     1.5    /* XML constructors */
     1.6  
     1.7 -  def spaces(n: Int): XML.Body = if (n == 0) Nil else List(XML.Text(Symbol.spaces(n)))
     1.8 -  val space: XML.Body = spaces(1)
     1.9 +  val space: XML.Body = List(XML.Text(Symbol.space))
    1.10 +  def spaces(n: Int): XML.Body =
    1.11 +    if (n == 0) Nil
    1.12 +    else if (n == 1) space
    1.13 +    else List(XML.Text(Symbol.spaces(n)))
    1.14  
    1.15    def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
    1.16      XML.Elem(Markup.Block(consistent, indent), body)
    1.17 @@ -45,79 +48,79 @@
    1.18  
    1.19    /* markup trees with physical blocks and breaks */
    1.20  
    1.21 -  sealed abstract class Tree { def length: Double }
    1.22 -  case class Block(
    1.23 +  private sealed abstract class Tree { def length: Double }
    1.24 +  private case class Block(
    1.25      markup: Option[(Markup, Option[XML.Body])],
    1.26      consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
    1.27 -  case class Str(string: String, length: Double) extends Tree
    1.28 -  case class Break(force: Boolean, width: Int, indent: Int) extends Tree
    1.29 +  private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
    1.30    { def length: Double = width.toDouble }
    1.31 +  private case class Str(string: String, length: Double) extends Tree
    1.32  
    1.33 -  val FBreak = Break(true, 1, 0)
    1.34 +  private val FBreak = Break(true, 1, 0)
    1.35  
    1.36 -  def make_block(
    1.37 +  private def make_block(
    1.38        markup: Option[(Markup, Option[XML.Body])],
    1.39        consistent: Boolean,
    1.40        indent: Int,
    1.41        body: List[Tree]): Tree =
    1.42      Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
    1.43  
    1.44 -  def make_tree(metric: Metric, xml: XML.Body): List[Tree] =
    1.45 -    xml flatMap {
    1.46 -      case XML.Wrapped_Elem(markup, body1, body2) =>
    1.47 -        List(make_block(Some(markup, Some(body1)), false, 0, make_tree(metric, body2)))
    1.48 -      case XML.Elem(markup, body) =>
    1.49 -        markup match {
    1.50 -          case Markup.Block(consistent, indent) =>
    1.51 -            List(make_block(None, consistent, indent, make_tree(metric, body)))
    1.52 -          case Markup.Break(width, indent) =>
    1.53 -            List(Break(false, width, indent))
    1.54 -          case Markup(Markup.ITEM, _) =>
    1.55 -            List(make_block(None, false, 2,
    1.56 -              make_tree(metric, XML.elem(Markup.BULLET, space) :: space ::: body)))
    1.57 -          case _ =>
    1.58 -            List(make_block(Some((markup, None)), false, 0, make_tree(metric, body)))
    1.59 -        }
    1.60 -      case XML.Text(text) =>
    1.61 -        Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
    1.62 +
    1.63 +  /* formatted output */
    1.64 +
    1.65 +  private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
    1.66 +  {
    1.67 +    def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
    1.68 +    def string(s: String, len: Double): Text =
    1.69 +      copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
    1.70 +    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
    1.71 +    def content: XML.Body = tx.reverse
    1.72 +  }
    1.73 +
    1.74 +  private def break_dist(trees: List[Tree], after: Double): Double =
    1.75 +    trees match {
    1.76 +      case (_: Break) :: _ => 0.0
    1.77 +      case t :: ts => t.length + break_dist(ts, after)
    1.78 +      case Nil => after
    1.79      }
    1.80  
    1.81 +  private def force_break(tree: Tree): Tree =
    1.82 +    tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
    1.83 +  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
    1.84  
    1.85 -  /* formatted output */
    1.86 +  private def force_next(trees: List[Tree]): List[Tree] =
    1.87 +    trees match {
    1.88 +      case Nil => Nil
    1.89 +      case (t: Break) :: ts => force_break(t) :: ts
    1.90 +      case t :: ts => t :: force_next(ts)
    1.91 +    }
    1.92  
    1.93    private val margin_default = 76.0
    1.94  
    1.95    def formatted(input: XML.Body, margin: Double = margin_default,
    1.96      metric: Metric = Metric_Default): XML.Body =
    1.97    {
    1.98 -    sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
    1.99 -    {
   1.100 -      def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
   1.101 -      def string(s: String, len: Double): Text =
   1.102 -        copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
   1.103 -      def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
   1.104 -      def content: XML.Body = tx.reverse
   1.105 -    }
   1.106 -
   1.107      val breakgain = margin / 20
   1.108      val emergencypos = (margin / 2).round.toInt
   1.109  
   1.110 -    def break_dist(trees: List[Tree], after: Double): Double =
   1.111 -      trees match {
   1.112 -        case (_: Break) :: _ => 0.0
   1.113 -        case t :: ts => t.length + break_dist(ts, after)
   1.114 -        case Nil => after
   1.115 -      }
   1.116 -
   1.117 -    def force_break(tree: Tree): Tree =
   1.118 -      tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
   1.119 -    def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
   1.120 -
   1.121 -    def force_next(trees: List[Tree]): List[Tree] =
   1.122 -      trees match {
   1.123 -        case Nil => Nil
   1.124 -        case (t: Break) :: ts => force_break(t) :: ts
   1.125 -        case t :: ts => t :: force_next(ts)
   1.126 +    def make_tree(inp: XML.Body): List[Tree] =
   1.127 +      inp flatMap {
   1.128 +        case XML.Wrapped_Elem(markup, body1, body2) =>
   1.129 +          List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
   1.130 +        case XML.Elem(markup, body) =>
   1.131 +          markup match {
   1.132 +            case Markup.Block(consistent, indent) =>
   1.133 +              List(make_block(None, consistent, indent, make_tree(body)))
   1.134 +            case Markup.Break(width, indent) =>
   1.135 +              List(Break(false, width, indent))
   1.136 +            case Markup(Markup.ITEM, _) =>
   1.137 +              List(make_block(None, false, 2,
   1.138 +                make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
   1.139 +            case _ =>
   1.140 +              List(make_block(Some((markup, None)), false, 0, make_tree(body)))
   1.141 +          }
   1.142 +        case XML.Text(text) =>
   1.143 +          Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
   1.144        }
   1.145  
   1.146      def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
   1.147 @@ -153,7 +156,7 @@
   1.148  
   1.149          case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
   1.150        }
   1.151 -    format(make_tree(metric, input), 0, 0.0, Text()).content
   1.152 +    format(make_tree(input), 0, 0.0, Text()).content
   1.153    }
   1.154  
   1.155    def string_of(input: XML.Body, margin: Double = margin_default,