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