src/Pure/General/output.ML
changeset 70662 0f9a4e8ee1ab
parent 65301 fca593a62785
child 70907 7e3f25a0cee4
equal deleted inserted replaced
70661:9c4809ec28ef 70662:0f9a4e8ee1ab
    33   val state: string -> unit
    33   val state: string -> unit
    34   val information: string -> unit
    34   val information: string -> unit
    35   val error_message': serial * string -> unit
    35   val error_message': serial * string -> unit
    36   val error_message: string -> unit
    36   val error_message: string -> unit
    37   val system_message: string -> unit
    37   val system_message: string -> unit
    38   val status: string -> unit
    38   val status: string list -> unit
    39   val report: string list -> unit
    39   val report: string list -> unit
    40   val result: Properties.T -> string list -> unit
    40   val result: Properties.T -> string list -> unit
    41   val protocol_message: Properties.T -> string list -> unit
    41   val protocol_message: Properties.T -> string list -> unit
    42   val try_protocol_message: Properties.T -> string list -> unit
    42   val try_protocol_message: Properties.T -> string list -> unit
    43 end;
    43 end;
   144 fun warning s = ! warning_fn [output s];
   144 fun warning s = ! warning_fn [output s];
   145 fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
   145 fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
   146 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
   146 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
   147 fun error_message s = error_message' (serial (), s);
   147 fun error_message s = error_message' (serial (), s);
   148 fun system_message s = ! system_message_fn [output s];
   148 fun system_message s = ! system_message_fn [output s];
   149 fun status s = ! status_fn [output s];
   149 fun status ss = ! status_fn (map output ss);
   150 fun report ss = ! report_fn (map output ss);
   150 fun report ss = ! report_fn (map output ss);
   151 fun result props ss = ! result_fn props (map output ss);
   151 fun result props ss = ! result_fn props (map output ss);
   152 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
   152 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
   153 fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
   153 fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
   154 
   154