src/Pure/General/pretty.ML
changeset 9730 11d137b25555
parent 9121 25245986e667
child 10952 b520e4f1313b
     1.1 --- a/src/Pure/General/pretty.ML	Tue Aug 29 20:12:54 2000 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Aug 29 20:13:17 2000 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    val str_list: string -> string -> string list -> T
     1.5    val big_list: string -> T list -> T
     1.6    val chunks: T list -> T
     1.7 +  val indent: int -> T -> T
     1.8    val string_of: T -> string
     1.9    val writeln: T -> unit
    1.10    val str_of: T -> string
    1.11 @@ -72,7 +73,10 @@
    1.12    | repstring a 1 = a
    1.13    | repstring a k =
    1.14        if k mod 2 = 0 then repstring(a^a) (k div 2)
    1.15 -                     else repstring(a^a) (k div 2) ^ a;
    1.16 +      else repstring(a^a) (k div 2) ^ a;
    1.17 +
    1.18 +val spaces = repstring " ";
    1.19 +
    1.20  
    1.21  (*** Type for lines of text: string, # of lines, position on line ***)
    1.22  
    1.23 @@ -81,7 +85,7 @@
    1.24  val emptytext = {tx = Buffer.empty, nl = 0, pos = 0};
    1.25  
    1.26  fun blanks wd {tx, nl, pos} =
    1.27 -    {tx  = Buffer.add (Symbol.output (repstring " " wd)) tx,
    1.28 +    {tx  = Buffer.add (Symbol.output (spaces wd)) tx,
    1.29       nl  = nl,
    1.30       pos = pos+wd};
    1.31  
    1.32 @@ -169,7 +173,7 @@
    1.33  
    1.34  fun block prts = blk (2, prts);
    1.35  
    1.36 -val strs = block o breaks o (map str);
    1.37 +val strs = block o breaks o map str;
    1.38  
    1.39  fun enclose lpar rpar prts =
    1.40    block (str lpar :: (prts @ [str rpar]));
    1.41 @@ -179,6 +183,9 @@
    1.42  fun big_list name prts = block (fbreaks (str name :: prts));
    1.43  fun chunks prts = blk (0, fbreaks prts);
    1.44  
    1.45 +fun indent 0 prt = prt
    1.46 +  | indent n prt = blk (0, [str (spaces n), prt]);
    1.47 +
    1.48  
    1.49  (*** Pretty printing with depth limitation ***)
    1.50  
    1.51 @@ -205,7 +212,7 @@
    1.52    let
    1.53      fun s_of (Block (prts, _, _)) = implode (map s_of prts)
    1.54        | s_of (String (s, _)) = s
    1.55 -      | s_of (Break (false, wd)) = Symbol.output (repstring " " wd)
    1.56 +      | s_of (Break (false, wd)) = Symbol.output (spaces wd)
    1.57        | s_of (Break (true, _)) = Symbol.output " ";
    1.58    in s_of (prune (! depth) prt) end;
    1.59