--- a/src/Pure/General/pretty.ML Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/General/pretty.ML Sat Dec 19 14:47:52 2015 +0100
@@ -12,10 +12,9 @@
breaking information. A "break" inserts a newline if the text until
the next break is too long to fit on the current line. After the newline,
text is indented to the level of the enclosing block. Normally, if a block
-is broken then all enclosing blocks will also be broken. Only "inconsistent
-breaks" are provided.
+is broken then all enclosing blocks will also be broken.
-The stored length of a block is used in breakdist (to treat each inner block as
+The stored length of a block is used in break_dist (to treat each inner block as
a unit for breaking).
*)
@@ -25,6 +24,7 @@
val default_indent: string -> int -> Output.output
val add_mode: string -> (string -> int -> Output.output) -> unit
type T
+ val make_block: Output.output * Output.output -> bool -> int -> T list -> T
val str: string -> T
val brk: int -> T
val brk_indent: int -> int -> T
@@ -34,7 +34,6 @@
val blk: int * T list -> T
val block: T list -> T
val strs: string list -> T
- val raw_markup: Output.output * Output.output -> int * T list -> T
val markup: Markup.T -> T list -> T
val mark: Markup.T -> T -> T
val mark_str: Markup.T * string -> T
@@ -124,16 +123,22 @@
(** printing items: compound phrases, strings, and breaks **)
abstype T =
- Block of (Output.output * Output.output) * T list * int * int
- (*markup output, body, indentation, length*)
+ Block of (Output.output * Output.output) * T list * bool * int * int
+ (*markup output, body, consistent, indentation, length*)
| String of Output.output * int (*text, length*)
| Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*)
with
-fun length (Block (_, _, _, len)) = len
+fun length (Block (_, _, _, _, len)) = len
| length (String (_, len)) = len
| length (Break (_, wd, _)) = wd;
+fun body_length [] len = len
+ | body_length (e :: es) len = body_length es (length e + len);
+
+fun make_block m consistent indent es = Block (m, es, consistent, indent, body_length es 0);
+fun markup_block m indent es = make_block (Markup.output m) false indent es;
+
(** derived operations to create formatting expressions **)
@@ -147,19 +152,11 @@
fun breaks prts = Library.separate (brk 1) prts;
fun fbreaks prts = Library.separate fbrk prts;
-fun raw_markup m (indent, es) =
- let
- fun sum [] k = k
- | sum (e :: es) k = sum es (length e + k);
- in Block (m, es, indent, sum es 0) end;
-
-fun markup_block m arg = raw_markup (Markup.output m) arg;
-
-val blk = markup_block Markup.empty;
+fun blk (ind, es) = markup_block Markup.empty ind es;
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
-fun markup m prts = markup_block m (0, prts);
+fun markup m = markup_block m 0;
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
@@ -200,7 +197,7 @@
| indent n prt = blk (0, [str (spaces n), prt]);
fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
- | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
+ | unbreakable (Block (m, es, _, indent, wd)) = Block (m, map unbreakable es, false, indent, wd)
| unbreakable (e as String _) = e;
@@ -249,16 +246,18 @@
(*Add the lengths of the expressions until the next Break; if no Break then
include "after", to account for text following this block.*)
-fun breakdist (Break _ :: _, _) = 0
- | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
- | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
- | breakdist ([], after) = after;
+fun break_dist (Break _ :: _, _) = 0
+ | break_dist (Block (_, _, _, _, len) :: es, after) = len + break_dist (es, after)
+ | break_dist (String (_, len) :: es, after) = len + break_dist (es, after)
+ | break_dist ([], after) = after;
+
+val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
+val force_all = map force_break;
(*Search for the next break (at this or higher levels) and force it to occur.*)
-val forcebreak = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
-fun forcenext [] = []
- | forcenext ((e as Break _) :: es) = forcebreak e :: es
- | forcenext (e :: es) = e :: forcenext es;
+fun force_next [] = []
+ | force_next ((e as Break _) :: es) = force_break e :: es
+ | force_next (e :: es) = e :: force_next es;
in
@@ -273,28 +272,30 @@
fun format ([], _, _) text = text
| format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
(case e of
- Block ((bg, en), bes, indent, _) =>
+ Block ((bg, en), bes, consistent, indent, blen) =>
let
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
val block' =
if pos' < emergencypos then (ind |> add_indent indent, pos')
else (add_indent pos'' Buffer.empty, pos'');
+ val d = break_dist (es, after)
+ val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
val btext: text = text
|> control bg
- |> format (bes, block', breakdist (es, after))
+ |> format (bes', block', d)
|> control en;
(*if this block was broken then force the next break*)
- val es' = if nl < #nl btext then forcenext es else es;
+ val es' = if nl < #nl btext then force_next es else es;
in format (es', block, after) btext end
| Break (force, wd, ind) =>
(*no break if text to next break fits on this line
or if breaking would add only breakgain to space*)
format (es, block, after)
(if not force andalso
- pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
- then text |> blanks wd (*just insert wd blanks*)
- else text |> newline |> indentation block |> blanks ind)
+ pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
+ then text |> blanks wd (*just insert wd blanks*)
+ else text |> newline |> indentation block |> blanks ind)
| String str => format (es, block, after) (string str text));
in
#tx (format ([input], (Buffer.empty, 0), 0) empty)
@@ -308,10 +309,10 @@
(*symbolic markup -- no formatting*)
fun symbolic prt =
let
- fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
- | out (Block ((bg, en), prts, indent, _)) =
+ fun out (Block ((bg, en), [], _, _, _)) = Buffer.add bg #> Buffer.add en
+ | out (Block ((bg, en), prts, consistent, indent, _)) =
Buffer.add bg #>
- Buffer.markup (Markup.block indent) (fold out prts) #>
+ Buffer.markup (Markup.block consistent indent) (fold out prts) #>
Buffer.add en
| out (String (s, _)) = Buffer.add s
| out (Break (false, wd, ind)) =
@@ -322,7 +323,7 @@
(*unformatted output*)
fun unformatted prt =
let
- fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
+ fun fmt (Block ((bg, en), prts, _, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
| fmt (String (s, _)) = Buffer.add s
| fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd);
in fmt prt Buffer.empty end;
@@ -379,11 +380,13 @@
(** ML toplevel pretty printing **)
-fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
+fun to_ML (Block (m, prts, consistent, indent, _)) =
+ ML_Pretty.Block (m, map to_ML prts, consistent, indent)
| to_ML (String s) = ML_Pretty.String s
| to_ML (Break b) = ML_Pretty.Break b;
-fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
+fun from_ML (ML_Pretty.Block (m, prts, consistent, indent)) =
+ make_block m consistent indent (map from_ML prts)
| from_ML (ML_Pretty.String s) = String s
| from_ML (ML_Pretty.Break b) = Break b;
--- a/src/Pure/General/pretty.scala Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/General/pretty.scala Sat Dec 19 14:47:52 2015 +0100
@@ -22,6 +22,10 @@
else space * k
}
+ def spaces_body(k: Int): XML.Body =
+ if (k == 0) Nil
+ else List(XML.Text(spaces(k)))
+
/* text metric -- standardized to width of space */
@@ -40,16 +44,16 @@
/* markup trees with physical blocks and breaks */
- def block(body: XML.Body): XML.Tree = Block(2, body)
+ def block(body: XML.Body): XML.Tree = Block(false, 2, body)
object Block
{
- def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup.Block(i), body)
+ def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+ XML.Elem(Markup.Block(consistent, indent), body)
- def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
+ def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] =
tree match {
- case XML.Elem(Markup.Block(i), body) => Some((i, body))
+ case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body))
case _ => None
}
}
@@ -57,7 +61,7 @@
object Break
{
def apply(w: Int, i: Int = 0): XML.Tree =
- XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w))))
+ XML.Elem(Markup.Break(w, i), spaces_body(w))
def unapply(tree: XML.Tree): Option[(Int, Int)] =
tree match {
@@ -69,7 +73,7 @@
val FBreak = XML.Text("\n")
def item(body: XML.Body): XML.Tree =
- Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
+ Block(false, 2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
@@ -98,7 +102,9 @@
sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
{
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
- def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
+ def string(s: String): Text =
+ if (s == "") this
+ else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
def blanks(wd: Int): Text = string(spaces(wd))
def content: XML.Body = tx.reverse
}
@@ -106,54 +112,63 @@
val breakgain = margin / 20
val emergencypos = (margin / 2).round.toInt
- def content_length(tree: XML.Tree): Double =
- XML.traverse_text(List(tree))(0.0)(_ + metric(_))
+ def content_length(body: XML.Body): Double =
+ XML.traverse_text(body)(0.0)(_ + metric(_))
- def breakdist(trees: XML.Body, after: Double): Double =
+ def break_dist(trees: XML.Body, after: Double): Double =
trees match {
case Break(_, _) :: _ => 0.0
case FBreak :: _ => 0.0
- case t :: ts => content_length(t) + breakdist(ts, after)
+ case t :: ts => content_length(List(t)) + break_dist(ts, after)
case Nil => after
}
- def forcenext(trees: XML.Body): XML.Body =
+ def force_all(trees: XML.Body): XML.Body =
+ trees flatMap {
+ case Break(_, ind) => FBreak :: spaces_body(ind)
+ case tree => List(tree)
+ }
+
+ def force_next(trees: XML.Body): XML.Body =
trees match {
case Nil => Nil
case FBreak :: _ => trees
- case Break(_, _) :: ts => FBreak :: ts
- case t :: ts => t :: forcenext(ts)
+ case Break(_, ind) :: ts => FBreak :: spaces_body(ind) ::: ts
+ case t :: ts => t :: force_next(ts)
}
def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
trees match {
case Nil => text
- case Block(indent, body) :: ts =>
+ case Block(consistent, indent, body) :: ts =>
val pos1 = (text.pos + indent).ceil.toInt
val pos2 = pos1 % emergencypos
val blockin1 =
if (pos1 < emergencypos) pos1
else pos2
- val btext = format(body, blockin1, breakdist(ts, after), text)
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val blen = content_length(body)
+ val d = break_dist(ts, after)
+ val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
+ val btext = format(body1, blockin1, d, text)
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
format(ts1, blockin, after, btext)
case Break(wd, ind) :: ts =>
- if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
+ if (text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
format(ts, blockin, after, text.blanks(wd))
else format(ts, blockin, after, text.newline.blanks(blockin + ind))
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
- val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val btext = format(body2, blockin, break_dist(ts, after), text.copy(tx = Nil))
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
case XML.Elem(markup, body) :: ts =>
- val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val btext = format(body, blockin, break_dist(ts, after), text.copy(tx = Nil))
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
@@ -174,8 +189,8 @@
{
def fmt(tree: XML.Tree): XML.Body =
tree match {
- case Block(_, body) => body.flatMap(fmt)
- case Break(wd, _) => List(XML.Text(spaces(wd)))
+ case Block(_, _, body) => body.flatMap(fmt)
+ case Break(wd, _) => spaces_body(wd)
case FBreak => List(XML.Text(space))
case XML.Wrapped_Elem(markup, body1, body2) =>
List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
--- a/src/Pure/ML-Systems/ml_pretty.ML Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/ML-Systems/ml_pretty.ML Sat Dec 19 14:47:52 2015 +0100
@@ -8,11 +8,11 @@
struct
datatype pretty =
- Block of (string * string) * pretty list * int |
+ Block of (string * string) * pretty list * bool * int |
String of string * int |
Break of bool * int * int;
-fun block prts = Block (("", ""), prts, 2);
+fun block prts = Block (("", ""), prts, false, 2);
fun str s = String (s, size s);
fun brk width = Break (false, width, 0);
--- a/src/Pure/ML-Systems/polyml.ML Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Sat Dec 19 14:47:52 2015 +0100
@@ -136,7 +136,7 @@
| convert _ (PolyML.PrettyBlock (_, _,
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
ML_Pretty.Break (true, 1, 0)
- | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
+ | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
let
fun property name default =
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
@@ -145,7 +145,7 @@
val bg = property "begin" "";
val en = property "end" "";
val len' = property "length" len;
- in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+ in ML_Pretty.Block ((bg, en), map (convert len') prts, consistent, ind) end
| convert len (PolyML.PrettyString s) =
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
in convert "" end;
@@ -154,11 +154,11 @@
| ml_pretty (ML_Pretty.Break (true, _, _)) =
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
[PolyML.PrettyString " "])
- | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+ | ml_pretty (ML_Pretty.Block ((bg, en), prts, consistent, ind)) =
let val context =
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
(if en = "" then [] else [PolyML.ContextProperty ("end", en)])
- in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
+ in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
| ml_pretty (ML_Pretty.String (s, len)) =
if len = size s then PolyML.PrettyString s
else PolyML.PrettyBlock
--- a/src/Pure/PIDE/markup.ML Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Dec 19 14:47:52 2015 +0100
@@ -64,8 +64,8 @@
val urlN: string val url: string -> T
val docN: string val doc: string -> T
val indentN: string
- val blockN: string val block: int -> T
val widthN: string
+ val blockN: string val block: bool -> int -> T
val breakN: string val break: int -> int -> T
val fbreakN: string val fbreak: T
val itemN: string val item: T
@@ -377,12 +377,21 @@
(* pretty printing *)
+val consistentN = "consistent";
val indentN = "indent";
-val (blockN, block) = markup_int "block" indentN;
+val widthN = "width";
-val widthN = "width";
+val blockN = "block";
+fun block c i =
+ (blockN,
+ (if c then [(consistentN, print_bool c)] else []) @
+ (if i <> 0 then [(indentN, print_int i)] else []));
+
val breakN = "break";
-fun break w i = (breakN, [(widthN, print_int w), (indentN, print_int i)]);
+fun break w i =
+ (breakN,
+ (if w <> 0 then [(widthN, print_int w)] else []) @
+ (if i <> 0 then [(indentN, print_int i)] else []));
val (fbreakN, fbreak) = markup_elem "fbreak";
--- a/src/Pure/PIDE/markup.scala Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Dec 19 14:47:52 2015 +0100
@@ -180,20 +180,38 @@
/* pretty printing */
+ val Consistent = new Properties.Boolean("consistent")
val Indent = new Properties.Int("indent")
- val Block = new Markup_Int("block", Indent.name)
+ val Width = new Properties.Int("width")
- val Width = new Properties.Int("width")
+ object Block
+ {
+ val name = "block"
+ def apply(c: Boolean, i: Int): Markup =
+ Markup(name,
+ (if (c) Consistent(c) else Nil) :::
+ (if (i != 0) Indent(i) else Nil))
+ def unapply(markup: Markup): Option[(Boolean, Int)] =
+ if (markup.name == name) {
+ val c = Consistent.unapply(markup.properties).getOrElse(false)
+ val i = Indent.unapply(markup.properties).getOrElse(0)
+ Some((c, i))
+ }
+ else None
+ }
+
object Break
{
val name = "break"
- def apply(w: Int, i: Int): Markup = Markup(name, Width(w) ::: Indent(i))
+ def apply(w: Int, i: Int): Markup =
+ Markup(name,
+ (if (w != 0) Width(w) else Nil) :::
+ (if (i != 0) Indent(i) else Nil))
def unapply(markup: Markup): Option[(Int, Int)] =
if (markup.name == name) {
- (markup.properties, markup.properties) match {
- case (Width(w), Indent(i)) => Some((w, i))
- case _ => None
- }
+ val w = Width.unapply(markup.properties).getOrElse(0)
+ val i = Indent.unapply(markup.properties).getOrElse(0)
+ Some((w, i))
}
else None
}
--- a/src/Pure/Syntax/syntax_phases.ML Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Dec 19 14:47:52 2015 +0100
@@ -750,7 +750,7 @@
let
val ((bg1, bg2), en) = typing_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
- in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
+ in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
else NONE
and ofsort_trans ty s =
@@ -758,7 +758,7 @@
let
val ((bg1, bg2), en) = sorting_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
- in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
+ in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
else NONE
and pretty_typ_ast m ast = ast