# HG changeset patch
# User wenzelm
# Date 1183893051 -7200
# Node ID e28b8e8a85b637005ca06c0a15cdd9c8733ef0bd
# Parent  32ee4111d1bccd9094d1e0c90b4c09642ce2525d
added markup for pretty printing;

diff -r 32ee4111d1bc -r e28b8e8a85b6 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Jul 08 12:20:56 2007 +0200
+++ b/src/Pure/General/markup.ML	Sun Jul 08 13:10:51 2007 +0200
@@ -13,6 +13,10 @@
   val pos_nameN: string
   type T = string * property list
   val none: T
+  val indentN: string
+  val blockN: string val block: int -> T
+  val breakN: string val break: int -> T
+  val fbreakN: string val fbreak: T
   val classN: string val class: string -> T
   val tyconN: string val tycon: string -> T
   val constN: string val const: string -> T
@@ -48,6 +52,18 @@
 
 fun markup kind = (kind, (kind, []): T);
 fun markup_name kind = (kind, fn name => (kind, [(nameN, name)]): T);
+fun markup_int kind prop = (kind, fn i => (kind, [(prop, string_of_int i)]): T);
+
+
+(* pretty printing *)
+
+val indentN = "indent";
+val (blockN, block) = markup_int "block" indentN;
+
+val widthN = "width";
+val (breakN, break) = markup_int "break" widthN;
+
+val (fbreakN, fbreak) = markup "fbreak";
 
 
 (* logical entities *)