support pretty break indent, like underlying ML systems;
authorwenzelm
Thu Dec 17 17:32:01 2015 +0100 (2015-12-17)
changeset 61862e2a9e46ac0fb
parent 61855 32a530a5c54c
child 61863 931792ce2d83
support pretty break indent, like underlying ML systems;
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/ML-Systems/smlnj.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/General/pretty.ML	Wed Dec 16 17:30:30 2015 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Thu Dec 17 17:32:01 2015 +0100
     1.3 @@ -27,6 +27,7 @@
     1.4    type T
     1.5    val str: string -> T
     1.6    val brk: int -> T
     1.7 +  val brk_indent: int -> int -> T
     1.8    val fbrk: T
     1.9    val breaks: T list -> T list
    1.10    val fbreaks: T list -> T list
    1.11 @@ -126,12 +127,12 @@
    1.12      Block of (Output.output * Output.output) * T list * int * int
    1.13        (*markup output, body, indentation, length*)
    1.14    | String of Output.output * int  (*text, length*)
    1.15 -  | Break of bool * int  (*mandatory flag, width if not taken*)
    1.16 +  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
    1.17  with
    1.18  
    1.19  fun length (Block (_, _, _, len)) = len
    1.20    | length (String (_, len)) = len
    1.21 -  | length (Break (_, wd)) = wd;
    1.22 +  | length (Break (_, wd, _)) = wd;
    1.23  
    1.24  
    1.25  
    1.26 @@ -139,8 +140,9 @@
    1.27  
    1.28  val str = String o Output.output_width;
    1.29  
    1.30 -fun brk wd = Break (false, wd);
    1.31 -val fbrk = Break (true, 1);
    1.32 +fun brk wd = Break (false, wd, 0);
    1.33 +fun brk_indent wd ind = Break (false, wd, ind);
    1.34 +val fbrk = Break (true, 1, 0);
    1.35  
    1.36  fun breaks prts = Library.separate (brk 1) prts;
    1.37  fun fbreaks prts = Library.separate fbrk prts;
    1.38 @@ -197,7 +199,7 @@
    1.39  fun indent 0 prt = prt
    1.40    | indent n prt = blk (0, [str (spaces n), prt]);
    1.41  
    1.42 -fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
    1.43 +fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
    1.44    | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
    1.45    | unbreakable (e as String _) = e;
    1.46  
    1.47 @@ -284,14 +286,14 @@
    1.48                  (*if this block was broken then force the next break*)
    1.49                  val es' = if nl < #nl btext then forcenext es else es;
    1.50                in format (es', block, after) btext end
    1.51 -          | Break (force, wd) =>
    1.52 +          | Break (force, wd, ind) =>
    1.53                (*no break if text to next break fits on this line
    1.54                  or if breaking would add only breakgain to space*)
    1.55                format (es, block, after)
    1.56                  (if not force andalso
    1.57                      pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
    1.58                    then text |> blanks wd  (*just insert wd blanks*)
    1.59 -                  else text |> newline |> indentation block)
    1.60 +                  else text |> newline |> indentation block |> blanks ind)
    1.61            | String str => format (es, block, after) (string str text));
    1.62    in
    1.63      #tx (format ([input], (Buffer.empty, 0), 0) empty)
    1.64 @@ -311,9 +313,9 @@
    1.65            Buffer.markup (Markup.block indent) (fold out prts) #>
    1.66            Buffer.add en
    1.67        | out (String (s, _)) = Buffer.add s
    1.68 -      | out (Break (false, wd)) =
    1.69 -          Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.70 -      | out (Break (true, _)) = Buffer.add (Output.output "\n");
    1.71 +      | out (Break (false, wd, ind)) =
    1.72 +          Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
    1.73 +      | out (Break (true, _, _)) = Buffer.add (Output.output "\n");
    1.74    in out prt Buffer.empty end;
    1.75  
    1.76  (*unformatted output*)
    1.77 @@ -321,7 +323,7 @@
    1.78    let
    1.79      fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
    1.80        | fmt (String (s, _)) = Buffer.add s
    1.81 -      | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
    1.82 +      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd);
    1.83    in fmt prt Buffer.empty end;
    1.84  
    1.85  
     2.1 --- a/src/Pure/General/pretty.scala	Wed Dec 16 17:30:30 2015 +0100
     2.2 +++ b/src/Pure/General/pretty.scala	Thu Dec 17 17:32:01 2015 +0100
     2.3 @@ -56,12 +56,12 @@
     2.4  
     2.5    object Break
     2.6    {
     2.7 -    def apply(w: Int): XML.Tree =
     2.8 -      XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
     2.9 +    def apply(w: Int, i: Int = 0): XML.Tree =
    2.10 +      XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w))))
    2.11  
    2.12 -    def unapply(tree: XML.Tree): Option[Int] =
    2.13 +    def unapply(tree: XML.Tree): Option[(Int, Int)] =
    2.14        tree match {
    2.15 -        case XML.Elem(Markup.Break(w), _) => Some(w)
    2.16 +        case XML.Elem(Markup.Break(w, i), _) => Some((w, i))
    2.17          case _ => None
    2.18        }
    2.19    }
    2.20 @@ -111,7 +111,7 @@
    2.21  
    2.22      def breakdist(trees: XML.Body, after: Double): Double =
    2.23        trees match {
    2.24 -        case Break(_) :: _ => 0.0
    2.25 +        case Break(_, _) :: _ => 0.0
    2.26          case FBreak :: _ => 0.0
    2.27          case t :: ts => content_length(t) + breakdist(ts, after)
    2.28          case Nil => after
    2.29 @@ -121,7 +121,7 @@
    2.30        trees match {
    2.31          case Nil => Nil
    2.32          case FBreak :: _ => trees
    2.33 -        case Break(_) :: ts => FBreak :: ts
    2.34 +        case Break(_, _) :: ts => FBreak :: ts
    2.35          case t :: ts => t :: forcenext(ts)
    2.36        }
    2.37  
    2.38 @@ -139,10 +139,10 @@
    2.39            val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    2.40            format(ts1, blockin, after, btext)
    2.41  
    2.42 -        case Break(wd) :: ts =>
    2.43 +        case Break(wd, ind) :: ts =>
    2.44            if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
    2.45              format(ts, blockin, after, text.blanks(wd))
    2.46 -          else format(ts, blockin, after, text.newline.blanks(blockin))
    2.47 +          else format(ts, blockin, after, text.newline.blanks(blockin + ind))
    2.48          case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
    2.49  
    2.50          case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
    2.51 @@ -175,7 +175,7 @@
    2.52      def fmt(tree: XML.Tree): XML.Body =
    2.53        tree match {
    2.54          case Block(_, body) => body.flatMap(fmt)
    2.55 -        case Break(wd) => List(XML.Text(spaces(wd)))
    2.56 +        case Break(wd, _) => List(XML.Text(spaces(wd)))
    2.57          case FBreak => List(XML.Text(space))
    2.58          case XML.Wrapped_Elem(markup, body1, body2) =>
    2.59            List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
     3.1 --- a/src/Pure/ML-Systems/ml_pretty.ML	Wed Dec 16 17:30:30 2015 +0100
     3.2 +++ b/src/Pure/ML-Systems/ml_pretty.ML	Thu Dec 17 17:32:01 2015 +0100
     3.3 @@ -10,11 +10,11 @@
     3.4  datatype pretty =
     3.5    Block of (string * string) * pretty list * int |
     3.6    String of string * int |
     3.7 -  Break of bool * int;
     3.8 +  Break of bool * int * int;
     3.9  
    3.10  fun block prts = Block (("", ""), prts, 2);
    3.11  fun str s = String (s, size s);
    3.12 -fun brk wd = Break (false, wd);
    3.13 +fun brk width = Break (false, width, 0);
    3.14  
    3.15  fun pair pretty1 pretty2 ((x, y), depth: int) =
    3.16    block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 16 17:30:30 2015 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Dec 17 17:32:01 2015 +0100
     4.3 @@ -132,10 +132,10 @@
     4.4  
     4.5  val pretty_ml =
     4.6    let
     4.7 -    fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
     4.8 +    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
     4.9        | convert _ (PolyML.PrettyBlock (_, _,
    4.10              [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
    4.11 -          ML_Pretty.Break (true, 1)
    4.12 +          ML_Pretty.Break (true, 1, 0)
    4.13        | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
    4.14            let
    4.15              fun property name default =
    4.16 @@ -150,8 +150,8 @@
    4.17            ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
    4.18    in convert "" end;
    4.19  
    4.20 -fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
    4.21 -  | ml_pretty (ML_Pretty.Break (true, _)) =
    4.22 +fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
    4.23 +  | ml_pretty (ML_Pretty.Break (true, _, _)) =
    4.24        PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
    4.25          [PolyML.PrettyString " "])
    4.26    | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Dec 16 17:30:30 2015 +0100
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Dec 17 17:32:01 2015 +0100
     5.3 @@ -119,8 +119,9 @@
     5.4            (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
     5.5              List.app pprint prts; PrettyPrint.closeBox pps; str en)
     5.6        | pprint (ML_Pretty.String (s, _)) = str s
     5.7 -      | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
     5.8 -      | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
     5.9 +      | pprint (ML_Pretty.Break (false, width, offset)) =
    5.10 +          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
    5.11 +      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
    5.12    in pprint end;
    5.13  
    5.14  fun toplevel_pp context path pp =
     6.1 --- a/src/Pure/PIDE/markup.ML	Wed Dec 16 17:30:30 2015 +0100
     6.2 +++ b/src/Pure/PIDE/markup.ML	Thu Dec 17 17:32:01 2015 +0100
     6.3 @@ -66,7 +66,7 @@
     6.4    val indentN: string
     6.5    val blockN: string val block: int -> T
     6.6    val widthN: string
     6.7 -  val breakN: string val break: int -> T
     6.8 +  val breakN: string val break: int -> int -> T
     6.9    val fbreakN: string val fbreak: T
    6.10    val itemN: string val item: T
    6.11    val wordsN: string val words: T
    6.12 @@ -381,7 +381,8 @@
    6.13  val (blockN, block) = markup_int "block" indentN;
    6.14  
    6.15  val widthN = "width";
    6.16 -val (breakN, break) = markup_int "break" widthN;
    6.17 +val breakN = "break";
    6.18 +fun break w i = (breakN, [(widthN, print_int w), (indentN, print_int i)]);
    6.19  
    6.20  val (fbreakN, fbreak) = markup_elem "fbreak";
    6.21  
     7.1 --- a/src/Pure/PIDE/markup.scala	Wed Dec 16 17:30:30 2015 +0100
     7.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 17 17:32:01 2015 +0100
     7.3 @@ -180,8 +180,23 @@
     7.4  
     7.5    /* pretty printing */
     7.6  
     7.7 -  val Block = new Markup_Int("block", "indent")
     7.8 -  val Break = new Markup_Int("break", "width")
     7.9 +  val Indent = new Properties.Int("indent")
    7.10 +  val Block = new Markup_Int("block", Indent.name)
    7.11 +
    7.12 +  val Width = new Properties.Int("width")
    7.13 +  object Break
    7.14 +  {
    7.15 +    val name = "break"
    7.16 +    def apply(w: Int, i: Int): Markup = Markup(name, Width(w) ::: Indent(i))
    7.17 +    def unapply(markup: Markup): Option[(Int, Int)] =
    7.18 +      if (markup.name == name) {
    7.19 +        (markup.properties, markup.properties) match {
    7.20 +          case (Width(w), Indent(i)) => Some((w, i))
    7.21 +          case _ => None
    7.22 +        }
    7.23 +      }
    7.24 +      else None
    7.25 +  }
    7.26  
    7.27    val ITEM = "item"
    7.28    val BULLET = "bullet"