src/Tools/Code/code_target.ML
changeset 32966 5b21661fe618
parent 32894 cdd7800de437
child 33522 737589bb9bb8
     1.1 --- a/src/Tools/Code/code_target.ML	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -60,9 +60,9 @@
     1.4  type serialization = destination -> (string * string option list) option;
     1.5  
     1.6  val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
     1.7 -fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
     1.8 +fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL (!code_width) f);
     1.9  fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
    1.10 -fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    1.11 +fun code_writeln p = Pretty.setmp_margin_CRITICAL (!code_width) Pretty.writeln p;
    1.12  
    1.13  (*FIXME why another code_setmp?*)
    1.14  fun compile f = (code_setmp f Compile; ());