--- 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 **)
--- a/src/Pure/pure_setup.ML Thu Jun 24 14:31:01 2010 +0200
+++ b/src/Pure/pure_setup.ML Thu Jun 24 14:31:46 2010 +0200
@@ -18,6 +18,7 @@
(* ML toplevel pretty printing *)
+toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";