# HG changeset patch
# User wenzelm
# Date 1142370395 -3600
# Node ID 2e8ad3f2cd66d3d9bea6702d86a4592d90f9b084
# Parent  cae36e16f3c071aec3a09d8916f228b0c4168f96
added command, keyword;
added chunks2;

diff -r cae36e16f3c0 -r 2e8ad3f2cd66 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Mar 14 22:06:33 2006 +0100
+++ b/src/Pure/General/pretty.ML	Tue Mar 14 22:06:35 2006 +0100
@@ -28,6 +28,8 @@
   type T
   val raw_str: string * real -> T
   val str: string -> T
+  val command: string -> T
+  val keyword: string -> T
   val brk: int -> T
   val fbrk: T
   val blk: int * T list -> T
@@ -37,6 +39,7 @@
   val block: T list -> T
   val strs: string list -> T
   val chunks: T list -> T
+  val chunks2: T list -> T
   val quote: T -> T
   val backquote: T -> T
   val separate: string -> T list -> T list
@@ -190,6 +193,9 @@
 fun raw_str (s, len) = String (s, Real.round len);
 val str = String o apsnd Real.round o Output.output_width;
 
+val command = String o apsnd Real.round o Output.keyword_width true;
+val keyword = String o apsnd Real.round o Output.keyword_width false;
+
 fun brk wd = Break (false, wd);
 val fbrk = Break (true, 2);
 
@@ -213,6 +219,7 @@
 
 val strs = block o breaks o map str;
 fun chunks prts = blk (0, fbreaks prts);
+fun chunks2 prts = blk (0, List.concat (Library.separate [fbrk, fbrk] (map single prts)));
 
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
 fun backquote prt = blk (1, [str "`", prt, str "`"]);