src/Tools/Code/code_target.ML
changeset 32740 9dd0a2f83429
parent 31957 a9742afd403e
child 32894 cdd7800de437
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    val code_of: theory -> string -> string
     1.5      -> string list -> (Code_Thingol.naming -> string list) -> string
     1.6    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
     1.7 -  val code_width: int ref
     1.8 +  val code_width: int Unsynchronized.ref
     1.9  
    1.10    val allow_abort: string -> theory -> theory
    1.11    val add_syntax_class: string -> class -> string option -> theory -> theory
    1.12 @@ -59,7 +59,7 @@
    1.13  datatype destination = Compile | Export | File of Path.T | String of string list;
    1.14  type serialization = destination -> (string * string option list) option;
    1.15  
    1.16 -val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.17 +val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.18  fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
    1.19  fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
    1.20  fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;