src/Pure/General/output.ML
changeset 62930 51ac6bc389e8
parent 62894 047129a6e200
child 63517 8ea738cffabe
     1.1 --- a/src/Pure/General/output.ML	Sat Apr 09 14:52:10 2016 +0200
     1.2 +++ b/src/Pure/General/output.ML	Sat Apr 09 16:16:05 2016 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/output.ML
     1.5 -    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     1.6 +    Author:     Makarius
     1.7  
     1.8 -Isabelle channels for diagnostic output.
     1.9 +Isabelle output channels.
    1.10  *)
    1.11  
    1.12  signature BASIC_OUTPUT =
    1.13 @@ -59,7 +59,7 @@
    1.14    val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    1.15  end;
    1.16  
    1.17 -structure Output: PRIVATE_OUTPUT =
    1.18 +structure Private_Output: PRIVATE_OUTPUT =
    1.19  struct
    1.20  
    1.21  (** print modes **)
    1.22 @@ -90,7 +90,23 @@
    1.23  
    1.24  (** output channels **)
    1.25  
    1.26 -(* raw output primitives -- not to be used in user-space *)
    1.27 +(* primitives -- provided via bootstrap environment *)
    1.28 +
    1.29 +val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
    1.30 +val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
    1.31 +val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
    1.32 +val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
    1.33 +val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
    1.34 +val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
    1.35 +val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
    1.36 +val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
    1.37 +val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
    1.38 +val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
    1.39 +val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
    1.40 +val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
    1.41 +
    1.42 +
    1.43 +(* physical output -- not to be used in user-space *)
    1.44  
    1.45  fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.46  fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    1.47 @@ -103,21 +119,18 @@
    1.48  
    1.49  exception Protocol_Message of Properties.T;
    1.50  
    1.51 -val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    1.52 -val state_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.53 -val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.54 -val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.55 -val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.56 -val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss);
    1.57 -
    1.58 -val error_message_fn =
    1.59 -  Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.60 -val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.61 -val status_fn = Unsynchronized.ref (fn _: output list => ());
    1.62 -val report_fn = Unsynchronized.ref (fn _: output list => ());
    1.63 -val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
    1.64 -val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
    1.65 -  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.66 +val _ =
    1.67 +  if Thread_Data.is_virtual then ()
    1.68 +  else
    1.69 +   (writeln_fn := (physical_writeln o implode);
    1.70 +    state_fn := (fn ss => ! writeln_fn ss);
    1.71 +    information_fn := (fn ss => ! writeln_fn ss);
    1.72 +    tracing_fn := (fn ss => ! writeln_fn ss);
    1.73 +    warning_fn := (physical_writeln o prefix_lines "### " o implode);
    1.74 +    legacy_fn := (fn ss => ! warning_fn ss);
    1.75 +    error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.76 +    system_message_fn := (fn ss => ! writeln_fn ss);
    1.77 +    protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
    1.78  
    1.79  fun writelns ss = ! writeln_fn (map output ss);
    1.80  fun writeln s = writelns [s];
    1.81 @@ -171,5 +184,6 @@
    1.82  
    1.83  end;
    1.84  
    1.85 +structure Output: OUTPUT = Private_Output;
    1.86  structure Basic_Output: BASIC_OUTPUT = Output;
    1.87  open Basic_Output;