--- a/src/Pure/General/pretty.ML Thu Jun 24 14:31:01 2010 +0200
+++ b/src/Pure/General/pretty.ML Thu Jun 24 14:31:46 2010 +0200
@@ -102,10 +102,11 @@
(** printing items: compound phrases, strings, and breaks **)
-datatype T =
+abstype T =
Block of (output * output) * T list * int * int | (*markup output, body, indentation, length*)
String of output * int | (*text, length*)
- Break of bool * int; (*mandatory flag, width if not taken*)
+ Break of bool * int (*mandatory flag, width if not taken*)
+with
fun length (Block (_, _, _, len)) = len
| length (String (_, len)) = len
@@ -323,6 +324,8 @@
| from_ML (ML_Pretty.String s) = String s
| from_ML (ML_Pretty.Break b) = Break b;
+end;
+
(** abstract pretty printing context **)