src/Tools/Code/code_printer.ML
changeset 37146 f652333bbf8e
parent 36960 01594f816e3a
child 37242 97097e589715
     1.1 --- a/src/Tools/Code/code_printer.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -105,19 +105,19 @@
     1.4  infixr 5 @|;
     1.5  fun x @@ y = [x, y];
     1.6  fun xs @| y = xs @ [y];
     1.7 -val str = PrintMode.setmp [] Pretty.str;
     1.8 +val str = Print_Mode.setmp [] Pretty.str;
     1.9  val concat = Pretty.block o Pretty.breaks;
    1.10 -fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
    1.11 +fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
    1.12  val brackets = enclose "(" ")" o Pretty.breaks;
    1.13 -fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
    1.14 +fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
    1.15  fun enum_default default sep l r [] = str default
    1.16    | enum_default default sep l r xs = enum sep l r xs;
    1.17  fun semicolon ps = Pretty.block [concat ps, str ";"];
    1.18  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    1.19 -fun indent i = PrintMode.setmp [] (Pretty.indent i);
    1.20 +fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    1.21  
    1.22 -fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
    1.23 -fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
    1.24 +fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
    1.25 +fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
    1.26  
    1.27  
    1.28  (** names and variable name contexts **)