# HG changeset patch # User wenzelm # Date 1450369921 -3600 # Node ID e2a9e46ac0fb2b7ac8f74e999a4a84f85a93ade1 # Parent 32a530a5c54cfa3bd5263600e3bdfae87153627e support pretty break indent, like underlying ML systems; diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/General/pretty.ML Thu Dec 17 17:32:01 2015 +0100 @@ -27,6 +27,7 @@ type T val str: string -> T val brk: int -> T + val brk_indent: int -> int -> T val fbrk: T val breaks: T list -> T list val fbreaks: T list -> T list @@ -126,12 +127,12 @@ Block of (Output.output * Output.output) * T list * int * int (*markup output, body, indentation, length*) | String of Output.output * int (*text, length*) - | Break of bool * int (*mandatory flag, width if not taken*) + | Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*) with fun length (Block (_, _, _, len)) = len | length (String (_, len)) = len - | length (Break (_, wd)) = wd; + | length (Break (_, wd, _)) = wd; @@ -139,8 +140,9 @@ val str = String o Output.output_width; -fun brk wd = Break (false, wd); -val fbrk = Break (true, 1); +fun brk wd = Break (false, wd, 0); +fun brk_indent wd ind = Break (false, wd, ind); +val fbrk = Break (true, 1, 0); fun breaks prts = Library.separate (brk 1) prts; fun fbreaks prts = Library.separate fbrk prts; @@ -197,7 +199,7 @@ fun indent 0 prt = prt | indent n prt = blk (0, [str (spaces n), prt]); -fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd) +fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd) | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd) | unbreakable (e as String _) = e; @@ -284,14 +286,14 @@ (*if this block was broken then force the next break*) val es' = if nl < #nl btext then forcenext es else es; in format (es', block, after) btext end - | Break (force, wd) => + | 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) + 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) @@ -311,9 +313,9 @@ Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en | out (String (s, _)) = Buffer.add s - | out (Break (false, wd)) = - Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd)) - | out (Break (true, _)) = Buffer.add (Output.output "\n"); + | out (Break (false, wd, ind)) = + Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd)) + | out (Break (true, _, _)) = Buffer.add (Output.output "\n"); in out prt Buffer.empty end; (*unformatted output*) @@ -321,7 +323,7 @@ let 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); + | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd); in fmt prt Buffer.empty end; diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/General/pretty.scala Thu Dec 17 17:32:01 2015 +0100 @@ -56,12 +56,12 @@ object Break { - def apply(w: Int): XML.Tree = - XML.Elem(Markup.Break(w), List(XML.Text(spaces(w)))) + def apply(w: Int, i: Int = 0): XML.Tree = + XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w)))) - def unapply(tree: XML.Tree): Option[Int] = + def unapply(tree: XML.Tree): Option[(Int, Int)] = tree match { - case XML.Elem(Markup.Break(w), _) => Some(w) + case XML.Elem(Markup.Break(w, i), _) => Some((w, i)) case _ => None } } @@ -111,7 +111,7 @@ def breakdist(trees: XML.Body, after: Double): Double = trees match { - case Break(_) :: _ => 0.0 + case Break(_, _) :: _ => 0.0 case FBreak :: _ => 0.0 case t :: ts => content_length(t) + breakdist(ts, after) case Nil => after @@ -121,7 +121,7 @@ trees match { case Nil => Nil case FBreak :: _ => trees - case Break(_) :: ts => FBreak :: ts + case Break(_, _) :: ts => FBreak :: ts case t :: ts => t :: forcenext(ts) } @@ -139,10 +139,10 @@ val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts format(ts1, blockin, after, btext) - case Break(wd) :: ts => + case Break(wd, ind) :: ts => if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain))) format(ts, blockin, after, text.blanks(wd)) - else format(ts, blockin, after, text.newline.blanks(blockin)) + 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 => @@ -175,7 +175,7 @@ def fmt(tree: XML.Tree): XML.Body = tree match { case Block(_, body) => body.flatMap(fmt) - case Break(wd) => List(XML.Text(spaces(wd))) + case Break(wd, _) => List(XML.Text(spaces(wd))) case FBreak => List(XML.Text(space)) case XML.Wrapped_Elem(markup, body1, body2) => List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt))) diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/ML-Systems/ml_pretty.ML --- a/src/Pure/ML-Systems/ml_pretty.ML Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/ML-Systems/ml_pretty.ML Thu Dec 17 17:32:01 2015 +0100 @@ -10,11 +10,11 @@ datatype pretty = Block of (string * string) * pretty list * int | String of string * int | - Break of bool * int; + Break of bool * int * int; fun block prts = Block (("", ""), prts, 2); fun str s = String (s, size s); -fun brk wd = Break (false, wd); +fun brk width = Break (false, width, 0); fun pair pretty1 pretty2 ((x, y), depth: int) = block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"]; diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Thu Dec 17 17:32:01 2015 +0100 @@ -132,10 +132,10 @@ val pretty_ml = let - fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd) + fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset) | convert _ (PolyML.PrettyBlock (_, _, [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = - ML_Pretty.Break (true, 1) + ML_Pretty.Break (true, 1, 0) | convert len (PolyML.PrettyBlock (ind, _, context, prts)) = let fun property name default = @@ -150,8 +150,8 @@ ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) in convert "" end; -fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) - | ml_pretty (ML_Pretty.Break (true, _)) = +fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset) + | ml_pretty (ML_Pretty.Break (true, _, _)) = PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], [PolyML.PrettyString " "]) | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Thu Dec 17 17:32:01 2015 +0100 @@ -119,8 +119,9 @@ (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind)); List.app pprint prts; PrettyPrint.closeBox pps; str en) | pprint (ML_Pretty.String (s, _)) = str s - | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0} - | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps; + | pprint (ML_Pretty.Break (false, width, offset)) = + PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset} + | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps; in pprint end; fun toplevel_pp context path pp = diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/PIDE/markup.ML Thu Dec 17 17:32:01 2015 +0100 @@ -66,7 +66,7 @@ val indentN: string val blockN: string val block: int -> T val widthN: string - val breakN: string val break: int -> T + val breakN: string val break: int -> int -> T val fbreakN: string val fbreak: T val itemN: string val item: T val wordsN: string val words: T @@ -381,7 +381,8 @@ val (blockN, block) = markup_int "block" indentN; val widthN = "width"; -val (breakN, break) = markup_int "break" widthN; +val breakN = "break"; +fun break w i = (breakN, [(widthN, print_int w), (indentN, print_int i)]); val (fbreakN, fbreak) = markup_elem "fbreak"; diff -r 32a530a5c54c -r e2a9e46ac0fb src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Dec 16 17:30:30 2015 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Dec 17 17:32:01 2015 +0100 @@ -180,8 +180,23 @@ /* pretty printing */ - val Block = new Markup_Int("block", "indent") - val Break = new Markup_Int("break", "width") + val Indent = new Properties.Int("indent") + val Block = new Markup_Int("block", Indent.name) + + val Width = new Properties.Int("width") + object Break + { + val name = "break" + def apply(w: Int, i: Int): Markup = Markup(name, Width(w) ::: Indent(i)) + 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 + } + } + else None + } val ITEM = "item" val BULLET = "bullet"