src/Pure/General/output.ML
changeset 65301 fca593a62785
parent 63517 8ea738cffabe
child 70662 0f9a4e8ee1ab
equal deleted inserted replaced
65300:c262653a3b88 65301:fca593a62785
    55   val system_message_fn: (output list -> unit) Unsynchronized.ref
    55   val system_message_fn: (output list -> unit) Unsynchronized.ref
    56   val status_fn: (output list -> unit) Unsynchronized.ref
    56   val status_fn: (output list -> unit) Unsynchronized.ref
    57   val report_fn: (output list -> unit) Unsynchronized.ref
    57   val report_fn: (output list -> unit) Unsynchronized.ref
    58   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    58   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    59   val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    59   val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
       
    60   val init_channels: unit -> unit
    60 end;
    61 end;
    61 
    62 
    62 structure Private_Output: PRIVATE_OUTPUT =
    63 structure Private_Output: PRIVATE_OUTPUT =
    63 struct
    64 struct
    64 
    65 
   117 
   118 
   118 (* Isabelle output channels *)
   119 (* Isabelle output channels *)
   119 
   120 
   120 exception Protocol_Message of Properties.T;
   121 exception Protocol_Message of Properties.T;
   121 
   122 
   122 val _ =
   123 fun init_channels () =
   123   if Thread_Data.is_virtual then ()
   124  (writeln_fn := (physical_writeln o implode);
   124   else
   125   state_fn := (fn ss => ! writeln_fn ss);
   125    (writeln_fn := (physical_writeln o implode);
   126   information_fn := Output_Primitives.ignore_outputs;
   126     state_fn := (fn ss => ! writeln_fn ss);
   127   tracing_fn := (fn ss => ! writeln_fn ss);
   127     tracing_fn := (fn ss => ! writeln_fn ss);
   128   warning_fn := (physical_writeln o prefix_lines "### " o implode);
   128     warning_fn := (physical_writeln o prefix_lines "### " o implode);
   129   legacy_fn := (fn ss => ! warning_fn ss);
   129     legacy_fn := (fn ss => ! warning_fn ss);
   130   error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   130     error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   131   system_message_fn := (fn ss => ! writeln_fn ss);
   131     system_message_fn := (fn ss => ! writeln_fn ss);
   132   status_fn := Output_Primitives.ignore_outputs;
   132     protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
   133   report_fn := Output_Primitives.ignore_outputs;
       
   134   result_fn := (fn _ => Output_Primitives.ignore_outputs);
       
   135   protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
       
   136 
       
   137 val _ = if Thread_Data.is_virtual then () else init_channels ();
   133 
   138 
   134 fun writelns ss = ! writeln_fn (map output ss);
   139 fun writelns ss = ! writeln_fn (map output ss);
   135 fun writeln s = writelns [s];
   140 fun writeln s = writelns [s];
   136 fun state s = ! state_fn [output s];
   141 fun state s = ! state_fn [output s];
   137 fun information s = ! information_fn [output s];
   142 fun information s = ! information_fn [output s];