1.1 --- a/src/Tools/Code/code_printer.ML	Wed Dec 23 10:09:06 2009 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Wed Dec 23 11:32:08 2009 +0100
     1.3 @@ -18,9 +18,12 @@
     1.4    val str: string -> Pretty.T
     1.5    val concat: Pretty.T list -> Pretty.T
     1.6    val brackets: Pretty.T list -> Pretty.T
     1.7 +  val enclose: string -> string -> Pretty.T list -> Pretty.T
     1.8 +  val enum: string -> string -> string -> Pretty.T list -> Pretty.T
     1.9 +  val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    1.10    val semicolon: Pretty.T list -> Pretty.T
    1.11    val doublesemicolon: Pretty.T list -> Pretty.T
    1.12 -  val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    1.13 +  val indent: int -> Pretty.T -> Pretty.T
    1.14    val string_of_pretty: int -> Pretty.T -> string
    1.15    val writeln_pretty: int -> Pretty.T -> unit
    1.16  
    1.17 @@ -99,11 +102,14 @@
    1.18  fun xs @| y = xs @ [y];
    1.19  val str = PrintMode.setmp [] Pretty.str;
    1.20  val concat = Pretty.block o Pretty.breaks;
    1.21 -val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
    1.22 +fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
    1.23 +val brackets = enclose "(" ")" o Pretty.breaks;
    1.24 +fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
    1.25 +fun enum_default default sep l r [] = str default
    1.26 +  | enum_default default sep l r xs = enum sep l r xs;
    1.27  fun semicolon ps = Pretty.block [concat ps, str ";"];
    1.28  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    1.29 -fun enum_default default sep opn cls [] = str default
    1.30 -  | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    1.31 +fun indent i = PrintMode.setmp [] (Pretty.indent i);
    1.32  
    1.33  fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n";
    1.34  fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p;
    1.35 @@ -198,7 +204,7 @@
    1.36    | fixity _ _ = true;
    1.37  
    1.38  fun gen_brackify _ [p] = p
    1.39 -  | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
    1.40 +  | gen_brackify true (ps as _::_) = enclose "(" ")" ps
    1.41    | gen_brackify false (ps as _::_) = Pretty.block ps;
    1.42  
    1.43  fun brackify fxy_ctxt =
    1.44 @@ -210,7 +216,7 @@
    1.45  fun brackify_block fxy_ctxt p1 ps p2 =
    1.46    let val p = Pretty.block_enclose (p1, p2) ps
    1.47    in if fixity BR fxy_ctxt
    1.48 -    then Pretty.enclose "(" ")" [p]
    1.49 +    then enclose "(" ")" [p]
    1.50      else p
    1.51    end;
    1.52