# HG changeset patch
# User wenzelm
# Date 1277382706 -7200
# Node ID a23e8aa853eb52d3eede25f1da0346e2e1a2e5fd
# Parent  42804fb5dd921338f7b2ad4d452c47f62fd1f818
treat Pretty.T as strictly abstract type;

diff -r 42804fb5dd92 -r a23e8aa853eb src/Pure/General/pretty.ML
--- 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 **)
diff -r 42804fb5dd92 -r a23e8aa853eb src/Pure/pure_setup.ML
--- 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";