# HG changeset patch # User wenzelm # Date 1450551172 -3600 # Node ID ba466ac335e3fb89325a3cdacdce17f3ff20da1f # Parent 8c0037ebab1a1e9afb641e30b671548e9976209b clarified underlying datatypes; diff -r 8c0037ebab1a -r ba466ac335e3 src/Pure/General/pretty.ML --- 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; diff -r 8c0037ebab1a -r ba466ac335e3 src/Pure/ML-Systems/ml_pretty.ML --- 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; - diff -r 8c0037ebab1a -r ba466ac335e3 src/Pure/ML-Systems/polyml.ML --- 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)]) diff -r 8c0037ebab1a -r ba466ac335e3 src/Pure/ML-Systems/smlnj.ML --- 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}