support pretty break indent, like underlying ML systems;

--- 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;
 
 

--- 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)))

--- 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 ")"];

--- 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)) =

--- 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 =

--- 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";
 

--- 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"