src/Pure/General/pretty.ML

   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
   val indent: int -> T -> T
   val unbreakable: T -> T
   val margin_default: int Unsynchronized.ref
+  val regularN: string
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
   val output: int option -> T -> Output.output
   val string_of_margin: int -> T -> string
   val string_of: T -> string

 
 (* output interfaces *)
 
 val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
 
+val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";
 
 fun output_buffer margin prt =
-  if print_mode_active symbolicN then symbolic prt
+  if print_mode_active symbolicN andalso not (print_mode_active regularN)
+  then symbolic prt
   else formatted (the_default (! margin_default) margin) prt;
 
 val output = Buffer.content oo output_buffer;
 fun string_of_margin margin = Output.escape o output (SOME margin);
 val string_of = Output.escape o output NONE;