support for blocks with consistent breaks;
authorwenzelm
Sat Dec 19 14:47:52 2015 +0100 (2015-12-19 ago)
changeset 618663a5992c3410c
parent 61865 931792ce2d83
child 61867 6dcc9e4f1aa6
support for blocks with consistent breaks;
tuned;
src/Pure/General/pretty.ML
src/Pure/General/pretty.scala
src/Pure/ML-Systems/ml_pretty.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sat Dec 19 10:59:14 2015 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Dec 19 14:47:52 2015 +0100
     1.3 @@ -12,10 +12,9 @@
     1.4  breaking information.  A "break" inserts a newline if the text until
     1.5  the next break is too long to fit on the current line.  After the newline,
     1.6  text is indented to the level of the enclosing block.  Normally, if a block
     1.7 -is broken then all enclosing blocks will also be broken.  Only "inconsistent
     1.8 -breaks" are provided.
     1.9 +is broken then all enclosing blocks will also be broken.
    1.10  
    1.11 -The stored length of a block is used in breakdist (to treat each inner block as
    1.12 +The stored length of a block is used in break_dist (to treat each inner block as
    1.13  a unit for breaking).
    1.14  *)
    1.15  
    1.16 @@ -25,6 +24,7 @@
    1.17    val default_indent: string -> int -> Output.output
    1.18    val add_mode: string -> (string -> int -> Output.output) -> unit
    1.19    type T
    1.20 +  val make_block: Output.output * Output.output -> bool -> int -> T list -> T
    1.21    val str: string -> T
    1.22    val brk: int -> T
    1.23    val brk_indent: int -> int -> T
    1.24 @@ -34,7 +34,6 @@
    1.25    val blk: int * T list -> T
    1.26    val block: T list -> T
    1.27    val strs: string list -> T
    1.28 -  val raw_markup: Output.output * Output.output -> int * T list -> T
    1.29    val markup: Markup.T -> T list -> T
    1.30    val mark: Markup.T -> T -> T
    1.31    val mark_str: Markup.T * string -> T
    1.32 @@ -124,16 +123,22 @@
    1.33  (** printing items: compound phrases, strings, and breaks **)
    1.34  
    1.35  abstype T =
    1.36 -    Block of (Output.output * Output.output) * T list * int * int
    1.37 -      (*markup output, body, indentation, length*)
    1.38 +    Block of (Output.output * Output.output) * T list * bool * int * int
    1.39 +      (*markup output, body, consistent, indentation, length*)
    1.40    | String of Output.output * int  (*text, length*)
    1.41    | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
    1.42  with
    1.43  
    1.44 -fun length (Block (_, _, _, len)) = len
    1.45 +fun length (Block (_, _, _, _, len)) = len
    1.46    | length (String (_, len)) = len
    1.47    | length (Break (_, wd, _)) = wd;
    1.48  
    1.49 +fun body_length [] len = len
    1.50 +  | body_length (e :: es) len = body_length es (length e + len);
    1.51 +
    1.52 +fun make_block m consistent indent es = Block (m, es, consistent, indent, body_length es 0);
    1.53 +fun markup_block m indent es = make_block (Markup.output m) false indent es;
    1.54 +
    1.55  
    1.56  
    1.57  (** derived operations to create formatting expressions **)
    1.58 @@ -147,19 +152,11 @@
    1.59  fun breaks prts = Library.separate (brk 1) prts;
    1.60  fun fbreaks prts = Library.separate fbrk prts;
    1.61  
    1.62 -fun raw_markup m (indent, es) =
    1.63 -  let
    1.64 -    fun sum [] k = k
    1.65 -      | sum (e :: es) k = sum es (length e + k);
    1.66 -  in Block (m, es, indent, sum es 0) end;
    1.67 -
    1.68 -fun markup_block m arg = raw_markup (Markup.output m) arg;
    1.69 -
    1.70 -val blk = markup_block Markup.empty;
    1.71 +fun blk (ind, es) = markup_block Markup.empty ind es;
    1.72  fun block prts = blk (2, prts);
    1.73  val strs = block o breaks o map str;
    1.74  
    1.75 -fun markup m prts = markup_block m (0, prts);
    1.76 +fun markup m = markup_block m 0;
    1.77  fun mark m prt = if m = Markup.empty then prt else markup m [prt];
    1.78  fun mark_str (m, s) = mark m (str s);
    1.79  fun marks_str (ms, s) = fold_rev mark ms (str s);
    1.80 @@ -200,7 +197,7 @@
    1.81    | indent n prt = blk (0, [str (spaces n), prt]);
    1.82  
    1.83  fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
    1.84 -  | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
    1.85 +  | unbreakable (Block (m, es, _, indent, wd)) = Block (m, map unbreakable es, false, indent, wd)
    1.86    | unbreakable (e as String _) = e;
    1.87  
    1.88  
    1.89 @@ -249,16 +246,18 @@
    1.90  
    1.91  (*Add the lengths of the expressions until the next Break; if no Break then
    1.92    include "after", to account for text following this block.*)
    1.93 -fun breakdist (Break _ :: _, _) = 0
    1.94 -  | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
    1.95 -  | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
    1.96 -  | breakdist ([], after) = after;
    1.97 +fun break_dist (Break _ :: _, _) = 0
    1.98 +  | break_dist (Block (_, _, _, _, len) :: es, after) = len + break_dist (es, after)
    1.99 +  | break_dist (String (_, len) :: es, after) = len + break_dist (es, after)
   1.100 +  | break_dist ([], after) = after;
   1.101 +
   1.102 +val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
   1.103 +val force_all = map force_break;
   1.104  
   1.105  (*Search for the next break (at this or higher levels) and force it to occur.*)
   1.106 -val forcebreak = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
   1.107 -fun forcenext [] = []
   1.108 -  | forcenext ((e as Break _) :: es) = forcebreak e :: es
   1.109 -  | forcenext (e :: es) = e :: forcenext es;
   1.110 +fun force_next [] = []
   1.111 +  | force_next ((e as Break _) :: es) = force_break e :: es
   1.112 +  | force_next (e :: es) = e :: force_next es;
   1.113  
   1.114  in
   1.115  
   1.116 @@ -273,28 +272,30 @@
   1.117      fun format ([], _, _) text = text
   1.118        | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
   1.119            (case e of
   1.120 -            Block ((bg, en), bes, indent, _) =>
   1.121 +            Block ((bg, en), bes, consistent, indent, blen) =>
   1.122                let
   1.123                  val pos' = pos + indent;
   1.124                  val pos'' = pos' mod emergencypos;
   1.125                  val block' =
   1.126                    if pos' < emergencypos then (ind |> add_indent indent, pos')
   1.127                    else (add_indent pos'' Buffer.empty, pos'');
   1.128 +                val d = break_dist (es, after)
   1.129 +                val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
   1.130                  val btext: text = text
   1.131                    |> control bg
   1.132 -                  |> format (bes, block', breakdist (es, after))
   1.133 +                  |> format (bes', block', d)
   1.134                    |> control en;
   1.135                  (*if this block was broken then force the next break*)
   1.136 -                val es' = if nl < #nl btext then forcenext es else es;
   1.137 +                val es' = if nl < #nl btext then force_next es else es;
   1.138                in format (es', block, after) btext end
   1.139            | Break (force, wd, ind) =>
   1.140                (*no break if text to next break fits on this line
   1.141                  or if breaking would add only breakgain to space*)
   1.142                format (es, block, after)
   1.143                  (if not force andalso
   1.144 -                    pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   1.145 -                  then text |> blanks wd  (*just insert wd blanks*)
   1.146 -                  else text |> newline |> indentation block |> blanks ind)
   1.147 +                    pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
   1.148 +                 then text |> blanks wd  (*just insert wd blanks*)
   1.149 +                 else text |> newline |> indentation block |> blanks ind)
   1.150            | String str => format (es, block, after) (string str text));
   1.151    in
   1.152      #tx (format ([input], (Buffer.empty, 0), 0) empty)
   1.153 @@ -308,10 +309,10 @@
   1.154  (*symbolic markup -- no formatting*)
   1.155  fun symbolic prt =
   1.156    let
   1.157 -    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
   1.158 -      | out (Block ((bg, en), prts, indent, _)) =
   1.159 +    fun out (Block ((bg, en), [], _, _, _)) = Buffer.add bg #> Buffer.add en
   1.160 +      | out (Block ((bg, en), prts, consistent, indent, _)) =
   1.161            Buffer.add bg #>
   1.162 -          Buffer.markup (Markup.block indent) (fold out prts) #>
   1.163 +          Buffer.markup (Markup.block consistent indent) (fold out prts) #>
   1.164            Buffer.add en
   1.165        | out (String (s, _)) = Buffer.add s
   1.166        | out (Break (false, wd, ind)) =
   1.167 @@ -322,7 +323,7 @@
   1.168  (*unformatted output*)
   1.169  fun unformatted prt =
   1.170    let
   1.171 -    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
   1.172 +    fun fmt (Block ((bg, en), prts, _, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
   1.173        | fmt (String (s, _)) = Buffer.add s
   1.174        | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd);
   1.175    in fmt prt Buffer.empty end;
   1.176 @@ -379,11 +380,13 @@
   1.177  
   1.178  (** ML toplevel pretty printing **)
   1.179  
   1.180 -fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   1.181 +fun to_ML (Block (m, prts, consistent, indent, _)) =
   1.182 +      ML_Pretty.Block (m, map to_ML prts, consistent, indent)
   1.183    | to_ML (String s) = ML_Pretty.String s
   1.184    | to_ML (Break b) = ML_Pretty.Break b;
   1.185  
   1.186 -fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
   1.187 +fun from_ML (ML_Pretty.Block (m, prts, consistent, indent)) =
   1.188 +      make_block m consistent indent (map from_ML prts)
   1.189    | from_ML (ML_Pretty.String s) = String s
   1.190    | from_ML (ML_Pretty.Break b) = Break b;
   1.191  
     2.1 --- a/src/Pure/General/pretty.scala	Sat Dec 19 10:59:14 2015 +0100
     2.2 +++ b/src/Pure/General/pretty.scala	Sat Dec 19 14:47:52 2015 +0100
     2.3 @@ -22,6 +22,10 @@
     2.4      else space * k
     2.5    }
     2.6  
     2.7 +  def spaces_body(k: Int): XML.Body =
     2.8 +    if (k == 0) Nil
     2.9 +    else List(XML.Text(spaces(k)))
    2.10 +
    2.11  
    2.12    /* text metric -- standardized to width of space */
    2.13  
    2.14 @@ -40,16 +44,16 @@
    2.15  
    2.16    /* markup trees with physical blocks and breaks */
    2.17  
    2.18 -  def block(body: XML.Body): XML.Tree = Block(2, body)
    2.19 +  def block(body: XML.Body): XML.Tree = Block(false, 2, body)
    2.20  
    2.21    object Block
    2.22    {
    2.23 -    def apply(i: Int, body: XML.Body): XML.Tree =
    2.24 -      XML.Elem(Markup.Block(i), body)
    2.25 +    def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
    2.26 +      XML.Elem(Markup.Block(consistent, indent), body)
    2.27  
    2.28 -    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
    2.29 +    def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] =
    2.30        tree match {
    2.31 -        case XML.Elem(Markup.Block(i), body) => Some((i, body))
    2.32 +        case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body))
    2.33          case _ => None
    2.34        }
    2.35    }
    2.36 @@ -57,7 +61,7 @@
    2.37    object Break
    2.38    {
    2.39      def apply(w: Int, i: Int = 0): XML.Tree =
    2.40 -      XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w))))
    2.41 +      XML.Elem(Markup.Break(w, i), spaces_body(w))
    2.42  
    2.43      def unapply(tree: XML.Tree): Option[(Int, Int)] =
    2.44        tree match {
    2.45 @@ -69,7 +73,7 @@
    2.46    val FBreak = XML.Text("\n")
    2.47  
    2.48    def item(body: XML.Body): XML.Tree =
    2.49 -    Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
    2.50 +    Block(false, 2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
    2.51  
    2.52    val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
    2.53    def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
    2.54 @@ -98,7 +102,9 @@
    2.55      sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
    2.56      {
    2.57        def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
    2.58 -      def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
    2.59 +      def string(s: String): Text =
    2.60 +        if (s == "") this
    2.61 +        else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
    2.62        def blanks(wd: Int): Text = string(spaces(wd))
    2.63        def content: XML.Body = tx.reverse
    2.64      }
    2.65 @@ -106,54 +112,63 @@
    2.66      val breakgain = margin / 20
    2.67      val emergencypos = (margin / 2).round.toInt
    2.68  
    2.69 -    def content_length(tree: XML.Tree): Double =
    2.70 -      XML.traverse_text(List(tree))(0.0)(_ + metric(_))
    2.71 +    def content_length(body: XML.Body): Double =
    2.72 +      XML.traverse_text(body)(0.0)(_ + metric(_))
    2.73  
    2.74 -    def breakdist(trees: XML.Body, after: Double): Double =
    2.75 +    def break_dist(trees: XML.Body, after: Double): Double =
    2.76        trees match {
    2.77          case Break(_, _) :: _ => 0.0
    2.78          case FBreak :: _ => 0.0
    2.79 -        case t :: ts => content_length(t) + breakdist(ts, after)
    2.80 +        case t :: ts => content_length(List(t)) + break_dist(ts, after)
    2.81          case Nil => after
    2.82        }
    2.83  
    2.84 -    def forcenext(trees: XML.Body): XML.Body =
    2.85 +    def force_all(trees: XML.Body): XML.Body =
    2.86 +      trees flatMap {
    2.87 +        case Break(_, ind) => FBreak :: spaces_body(ind)
    2.88 +        case tree => List(tree)
    2.89 +      }
    2.90 +
    2.91 +    def force_next(trees: XML.Body): XML.Body =
    2.92        trees match {
    2.93          case Nil => Nil
    2.94          case FBreak :: _ => trees
    2.95 -        case Break(_, _) :: ts => FBreak :: ts
    2.96 -        case t :: ts => t :: forcenext(ts)
    2.97 +        case Break(_, ind) :: ts => FBreak :: spaces_body(ind) ::: ts
    2.98 +        case t :: ts => t :: force_next(ts)
    2.99        }
   2.100  
   2.101      def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
   2.102        trees match {
   2.103          case Nil => text
   2.104  
   2.105 -        case Block(indent, body) :: ts =>
   2.106 +        case Block(consistent, indent, body) :: ts =>
   2.107            val pos1 = (text.pos + indent).ceil.toInt
   2.108            val pos2 = pos1 % emergencypos
   2.109            val blockin1 =
   2.110              if (pos1 < emergencypos) pos1
   2.111              else pos2
   2.112 -          val btext = format(body, blockin1, breakdist(ts, after), text)
   2.113 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   2.114 +          val blen = content_length(body)
   2.115 +          val d = break_dist(ts, after)
   2.116 +          val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
   2.117 +          val btext = format(body1, blockin1, d, text)
   2.118 +          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
   2.119            format(ts1, blockin, after, btext)
   2.120  
   2.121          case Break(wd, ind) :: ts =>
   2.122 -          if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
   2.123 +          if (text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
   2.124              format(ts, blockin, after, text.blanks(wd))
   2.125            else format(ts, blockin, after, text.newline.blanks(blockin + ind))
   2.126          case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
   2.127  
   2.128          case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
   2.129 -          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
   2.130 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   2.131 +          val btext = format(body2, blockin, break_dist(ts, after), text.copy(tx = Nil))
   2.132 +          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
   2.133            val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
   2.134            format(ts1, blockin, after, btext1)
   2.135  
   2.136          case XML.Elem(markup, body) :: ts =>
   2.137 -          val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
   2.138 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   2.139 +          val btext = format(body, blockin, break_dist(ts, after), text.copy(tx = Nil))
   2.140 +          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
   2.141            val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
   2.142            format(ts1, blockin, after, btext1)
   2.143  
   2.144 @@ -174,8 +189,8 @@
   2.145    {
   2.146      def fmt(tree: XML.Tree): XML.Body =
   2.147        tree match {
   2.148 -        case Block(_, body) => body.flatMap(fmt)
   2.149 -        case Break(wd, _) => List(XML.Text(spaces(wd)))
   2.150 +        case Block(_, _, body) => body.flatMap(fmt)
   2.151 +        case Break(wd, _) => spaces_body(wd)
   2.152          case FBreak => List(XML.Text(space))
   2.153          case XML.Wrapped_Elem(markup, body1, body2) =>
   2.154            List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
     3.1 --- a/src/Pure/ML-Systems/ml_pretty.ML	Sat Dec 19 10:59:14 2015 +0100
     3.2 +++ b/src/Pure/ML-Systems/ml_pretty.ML	Sat Dec 19 14:47:52 2015 +0100
     3.3 @@ -8,11 +8,11 @@
     3.4  struct
     3.5  
     3.6  datatype pretty =
     3.7 -  Block of (string * string) * pretty list * int |
     3.8 +  Block of (string * string) * pretty list * bool * int |
     3.9    String of string * int |
    3.10    Break of bool * int * int;
    3.11  
    3.12 -fun block prts = Block (("", ""), prts, 2);
    3.13 +fun block prts = Block (("", ""), prts, false, 2);
    3.14  fun str s = String (s, size s);
    3.15  fun brk width = Break (false, width, 0);
    3.16  
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Dec 19 10:59:14 2015 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Dec 19 14:47:52 2015 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4        | convert _ (PolyML.PrettyBlock (_, _,
     4.5              [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
     4.6            ML_Pretty.Break (true, 1, 0)
     4.7 -      | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
     4.8 +      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
     4.9            let
    4.10              fun property name default =
    4.11                (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
    4.12 @@ -145,7 +145,7 @@
    4.13              val bg = property "begin" "";
    4.14              val en = property "end" "";
    4.15              val len' = property "length" len;
    4.16 -          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
    4.17 +          in ML_Pretty.Block ((bg, en), map (convert len') prts, consistent, ind) end
    4.18        | convert len (PolyML.PrettyString s) =
    4.19            ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
    4.20    in convert "" end;
    4.21 @@ -154,11 +154,11 @@
    4.22    | ml_pretty (ML_Pretty.Break (true, _, _)) =
    4.23        PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
    4.24          [PolyML.PrettyString " "])
    4.25 -  | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
    4.26 +  | ml_pretty (ML_Pretty.Block ((bg, en), prts, consistent, ind)) =
    4.27        let val context =
    4.28          (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
    4.29          (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
    4.30 -      in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
    4.31 +      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
    4.32    | ml_pretty (ML_Pretty.String (s, len)) =
    4.33        if len = size s then PolyML.PrettyString s
    4.34        else PolyML.PrettyBlock
     5.1 --- a/src/Pure/PIDE/markup.ML	Sat Dec 19 10:59:14 2015 +0100
     5.2 +++ b/src/Pure/PIDE/markup.ML	Sat Dec 19 14:47:52 2015 +0100
     5.3 @@ -64,8 +64,8 @@
     5.4    val urlN: string val url: string -> T
     5.5    val docN: string val doc: string -> T
     5.6    val indentN: string
     5.7 -  val blockN: string val block: int -> T
     5.8    val widthN: string
     5.9 +  val blockN: string val block: bool -> int -> T
    5.10    val breakN: string val break: int -> int -> T
    5.11    val fbreakN: string val fbreak: T
    5.12    val itemN: string val item: T
    5.13 @@ -377,12 +377,21 @@
    5.14  
    5.15  (* pretty printing *)
    5.16  
    5.17 +val consistentN = "consistent";
    5.18  val indentN = "indent";
    5.19 -val (blockN, block) = markup_int "block" indentN;
    5.20 +val widthN = "width";
    5.21  
    5.22 -val widthN = "width";
    5.23 +val blockN = "block";
    5.24 +fun block c i =
    5.25 +  (blockN,
    5.26 +    (if c then [(consistentN, print_bool c)] else []) @
    5.27 +    (if i <> 0 then [(indentN, print_int i)] else []));
    5.28 +
    5.29  val breakN = "break";
    5.30 -fun break w i = (breakN, [(widthN, print_int w), (indentN, print_int i)]);
    5.31 +fun break w i =
    5.32 +  (breakN,
    5.33 +    (if w <> 0 then [(widthN, print_int w)] else []) @
    5.34 +    (if i <> 0 then [(indentN, print_int i)] else []));
    5.35  
    5.36  val (fbreakN, fbreak) = markup_elem "fbreak";
    5.37  
     6.1 --- a/src/Pure/PIDE/markup.scala	Sat Dec 19 10:59:14 2015 +0100
     6.2 +++ b/src/Pure/PIDE/markup.scala	Sat Dec 19 14:47:52 2015 +0100
     6.3 @@ -180,20 +180,38 @@
     6.4  
     6.5    /* pretty printing */
     6.6  
     6.7 +  val Consistent = new Properties.Boolean("consistent")
     6.8    val Indent = new Properties.Int("indent")
     6.9 -  val Block = new Markup_Int("block", Indent.name)
    6.10 +  val Width = new Properties.Int("width")
    6.11  
    6.12 -  val Width = new Properties.Int("width")
    6.13 +  object Block
    6.14 +  {
    6.15 +    val name = "block"
    6.16 +    def apply(c: Boolean, i: Int): Markup =
    6.17 +      Markup(name,
    6.18 +        (if (c) Consistent(c) else Nil) :::
    6.19 +        (if (i != 0) Indent(i) else Nil))
    6.20 +    def unapply(markup: Markup): Option[(Boolean, Int)] =
    6.21 +      if (markup.name == name) {
    6.22 +        val c = Consistent.unapply(markup.properties).getOrElse(false)
    6.23 +        val i = Indent.unapply(markup.properties).getOrElse(0)
    6.24 +        Some((c, i))
    6.25 +      }
    6.26 +      else None
    6.27 +  }
    6.28 +
    6.29    object Break
    6.30    {
    6.31      val name = "break"
    6.32 -    def apply(w: Int, i: Int): Markup = Markup(name, Width(w) ::: Indent(i))
    6.33 +    def apply(w: Int, i: Int): Markup =
    6.34 +      Markup(name,
    6.35 +        (if (w != 0) Width(w) else Nil) :::
    6.36 +        (if (i != 0) Indent(i) else Nil))
    6.37      def unapply(markup: Markup): Option[(Int, Int)] =
    6.38        if (markup.name == name) {
    6.39 -        (markup.properties, markup.properties) match {
    6.40 -          case (Width(w), Indent(i)) => Some((w, i))
    6.41 -          case _ => None
    6.42 -        }
    6.43 +        val w = Width.unapply(markup.properties).getOrElse(0)
    6.44 +        val i = Indent.unapply(markup.properties).getOrElse(0)
    6.45 +        Some((w, i))
    6.46        }
    6.47        else None
    6.48    }
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Dec 19 10:59:14 2015 +0100
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Dec 19 14:47:52 2015 +0100
     7.3 @@ -750,7 +750,7 @@
     7.4          let
     7.5            val ((bg1, bg2), en) = typing_elem;
     7.6            val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
     7.7 -        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
     7.8 +        in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
     7.9        else NONE
    7.10  
    7.11      and ofsort_trans ty s =
    7.12 @@ -758,7 +758,7 @@
    7.13          let
    7.14            val ((bg1, bg2), en) = sorting_elem;
    7.15            val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
    7.16 -        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
    7.17 +        in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
    7.18        else NONE
    7.19  
    7.20      and pretty_typ_ast m ast = ast