clarified underlying datatypes;

--- a/src/Pure/General/pretty.ML	Sat Dec 19 19:07:14 2015 +0100
+++ b/src/Pure/General/pretty.ML	Sat Dec 19 19:52:52 2015 +0100
@@ -108,8 +108,8 @@
 (** printing items: compound phrases, strings, and breaks **)
 
 abstype T =
-    Block of (Output.output * Output.output) * T list * bool * int * int
-      (*markup output, body, consistent, indentation, length*)
+    Block of (Output.output * Output.output) * bool * int * T list * int
+      (*markup output, consistent, indentation, body, length*)
   | String of Output.output * int  (*text, length*)
   | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
 with
@@ -121,7 +121,7 @@
 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 make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0);
 fun markup_block m indent es = make_block (Markup.output m) false indent es;
 
 
@@ -182,7 +182,8 @@
   | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
 
 fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
-  | unbreakable (Block (m, es, _, indent, wd)) = Block (m, map unbreakable es, false, indent, wd)
+  | unbreakable (Block (m, consistent, indent, es, len)) =
+      Block (m, consistent, indent, map unbreakable es, len)
   | unbreakable (e as String _) = e;
 
 
@@ -257,7 +258,7 @@
     fun format ([], _, _) text = text
       | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
           (case e of
-            Block ((bg, en), bes, consistent, indent, blen) =>
+            Block ((bg, en), consistent, indent, bes, blen) =>
               let
                 val pos' = pos + indent;
                 val pos'' = pos' mod emergencypos;
@@ -294,8 +295,8 @@
 (*symbolic markup -- no formatting*)
 fun symbolic prt =
   let
-    fun out (Block ((bg, en), [], _, _, _)) = Buffer.add bg #> Buffer.add en
-      | out (Block ((bg, en), prts, consistent, indent, _)) =
+    fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
+      | out (Block ((bg, en), consistent, indent, prts, _)) =
           Buffer.add bg #>
           Buffer.markup (Markup.block consistent indent) (fold out prts) #>
           Buffer.add en
@@ -308,7 +309,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;
@@ -365,12 +366,12 @@
 
 (** ML toplevel pretty printing **)
 
-fun to_ML (Block (m, prts, consistent, indent, _)) =
-      ML_Pretty.Block (m, map to_ML prts, consistent, indent)
+fun to_ML (Block (m, consistent, indent, prts, _)) =
+      ML_Pretty.Block (m, consistent, indent, map to_ML prts)
   | to_ML (String s) = ML_Pretty.String s
   | to_ML (Break b) = ML_Pretty.Break b;
 
-fun from_ML (ML_Pretty.Block (m, prts, consistent, indent)) =
+fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
       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/ML-Systems/ml_pretty.ML	Sat Dec 19 19:07:14 2015 +0100
+++ b/src/Pure/ML-Systems/ml_pretty.ML	Sat Dec 19 19:52:52 2015 +0100
@@ -8,11 +8,11 @@
 struct
 
 datatype pretty =
-  Block of (string * string) * pretty list * bool * int |
+  Block of (string * string) * bool * int * pretty list |
   String of string * int |
   Break of bool * int * int;
 
-fun block prts = Block (("", ""), prts, false, 2);
+fun block prts = Block (("", ""), false, 2, prts);
 fun str s = String (s, size s);
 fun brk width = Break (false, width, 0);
 
@@ -28,4 +28,3 @@
   in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
 
 end;
-

--- a/src/Pure/ML-Systems/polyml.ML	Sat Dec 19 19:07:14 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Dec 19 19:52:52 2015 +0100
@@ -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, consistent, ind) end
+          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) 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,7 +154,7 @@
   | ml_pretty (ML_Pretty.Break (true, _, _)) =
       PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
         [PolyML.PrettyString " "])
-  | ml_pretty (ML_Pretty.Block ((bg, en), prts, consistent, ind)) =
+  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
       let val context =
         (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
         (if en = "" then [] else [PolyML.ContextProperty ("end", en)])

--- a/src/Pure/ML-Systems/smlnj.ML	Sat Dec 19 19:07:14 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Dec 19 19:52:52 2015 +0100
@@ -115,9 +115,12 @@
   let
     fun str "" = ()
       | str s = PrettyPrint.string pps s;
-    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
-          (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
-            List.app pprint prts; PrettyPrint.closeBox pps; str en)
+    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
+         (str bg;
+          (if consistent then PrettyPrint.openHVBox else 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, width, offset)) =
           PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}