(*  Title:      Pure/General/output.ML

     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)

 Isabelle output channels.

 *)

 signature BASIC_OUTPUT =

 sig

   val writeln: string -> unit

   val tracing: string -> unit

   val warning: string -> unit

   val legacy_feature: string -> unit

 end;

 signature OUTPUT =

 sig

   include BASIC_OUTPUT

   type output = string

   val default_output: string -> output * int

   val default_escape: output -> string

   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit

   val output_width: string -> output * int

   val output: string -> output

   val escape: output -> string

   val raw_stdout: output -> unit

   val raw_stderr: output -> unit

   val raw_writeln: output -> unit

   structure Private_Hooks:

   sig

     val writeln_fn: (output -> unit) Unsynchronized.ref

     val urgent_message_fn: (output -> unit) Unsynchronized.ref

     val tracing_fn: (output -> unit) Unsynchronized.ref

     val warning_fn: (output -> unit) Unsynchronized.ref

     val error_fn: (output -> unit) Unsynchronized.ref

     val prompt_fn: (output -> unit) Unsynchronized.ref

     val status_fn: (output -> unit) Unsynchronized.ref

     val report_fn: (output -> unit) Unsynchronized.ref

   end

   val urgent_message: string -> unit

   val error_msg: string -> unit

   val prompt: string -> unit

   val status: string -> unit

   val report: string -> unit

 end;

 structure Output: OUTPUT =

 struct

 (** print modes **)

 type output = string;  (*raw system output*)

 fun default_output s = (s, size s);

 fun default_escape (s: output) = s;

 local

   val default = {output = default_output, escape = default_escape};

   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);

 in

   fun add_mode name output escape =

     Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));

   fun get_mode () =

     the_default default

       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));

 end;

 fun output_width x = #output (get_mode ()) x;

 val output = #1 o output_width;

 fun escape x = #escape (get_mode ()) x;

 (** output channels **)

 (* raw output primitives -- not to be used in user-space *)

 fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);

 fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);

 fun raw_writeln "" = ()

   | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)

 (* Isabelle output channels *)

 structure Private_Hooks =

 struct

   val writeln_fn = Unsynchronized.ref raw_writeln;

   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);

   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);

   val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");

   val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");

   val prompt_fn = Unsynchronized.ref raw_stdout;

   val status_fn = Unsynchronized.ref (fn _: string => ());

   val report_fn = Unsynchronized.ref (fn _: string => ());

 end;

 fun writeln s = ! Private_Hooks.writeln_fn (output s);

 fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);

 fun tracing s = ! Private_Hooks.tracing_fn (output s);

 fun warning s = ! Private_Hooks.warning_fn (output s);

 fun error_msg s = ! Private_Hooks.error_fn (output s);

 fun prompt s = ! Private_Hooks.prompt_fn (output s);

 fun status s = ! Private_Hooks.status_fn (output s);

 fun report s = ! Private_Hooks.report_fn (output s);

 fun legacy_feature s = warning ("Legacy feature! " ^ s);

 end;

 structure Basic_Output: BASIC_OUTPUT = Output;

 open Basic_Output;