src/Pure/General/pretty.ML
changeset 72305 9c0b835d4cc2
parent 71678 910a081cca74
equal deleted inserted replaced
72304:f3e1144a1cec 72305:9c0b835d4cc2
    58   val str_list: string -> string -> string list -> T
    58   val str_list: string -> string -> string list -> T
    59   val big_list: string -> T list -> T
    59   val big_list: string -> T list -> T
    60   val indent: int -> T -> T
    60   val indent: int -> T -> T
    61   val unbreakable: T -> T
    61   val unbreakable: T -> T
    62   val margin_default: int Unsynchronized.ref
    62   val margin_default: int Unsynchronized.ref
       
    63   val regularN: string
    63   val symbolicN: string
    64   val symbolicN: string
    64   val output_buffer: int option -> T -> Buffer.T
    65   val output_buffer: int option -> T -> Buffer.T
    65   val output: int option -> T -> Output.output
    66   val output: int option -> T -> Output.output
    66   val string_of_margin: int -> T -> string
    67   val string_of_margin: int -> T -> string
    67   val string_of: T -> string
    68   val string_of: T -> string
   344 
   345 
   345 (* output interfaces *)
   346 (* output interfaces *)
   346 
   347 
   347 val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
   348 val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
   348 
   349 
       
   350 val regularN = "pretty_regular";
   349 val symbolicN = "pretty_symbolic";
   351 val symbolicN = "pretty_symbolic";
   350 
   352 
   351 fun output_buffer margin prt =
   353 fun output_buffer margin prt =
   352   if print_mode_active symbolicN then symbolic prt
   354   if print_mode_active symbolicN andalso not (print_mode_active regularN)
       
   355   then symbolic prt
   353   else formatted (the_default (! margin_default) margin) prt;
   356   else formatted (the_default (! margin_default) margin) prt;
   354 
   357 
   355 val output = Buffer.content oo output_buffer;
   358 val output = Buffer.content oo output_buffer;
   356 fun string_of_margin margin = Output.escape o output (SOME margin);
   359 fun string_of_margin margin = Output.escape o output (SOME margin);
   357 val string_of = Output.escape o output NONE;
   360 val string_of = Output.escape o output NONE;