src/Pure/General/output.ML
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
parent 43746 a41f618c641d
child 43760 ef8375a4dae4
permissions -rw-r--r--
JVM method invocation service via Scala layer;
     1 (*  Title:      Pure/General/output.ML
     2     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     3 
     4 Isabelle output channels.
     5 *)
     6 
     7 signature BASIC_OUTPUT =
     8 sig
     9   val writeln: string -> unit
    10   val tracing: string -> unit
    11   val warning: string -> unit
    12   val legacy_feature: string -> unit
    13 end;
    14 
    15 signature OUTPUT =
    16 sig
    17   include BASIC_OUTPUT
    18   type output = string
    19   val default_output: string -> output * int
    20   val default_escape: output -> string
    21   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
    22   val output_width: string -> output * int
    23   val output: string -> output
    24   val escape: output -> string
    25   val raw_stdout: output -> unit
    26   val raw_stderr: output -> unit
    27   val raw_writeln: output -> unit
    28   structure Private_Hooks:
    29   sig
    30     val writeln_fn: (output -> unit) Unsynchronized.ref
    31     val urgent_message_fn: (output -> unit) Unsynchronized.ref
    32     val tracing_fn: (output -> unit) Unsynchronized.ref
    33     val warning_fn: (output -> unit) Unsynchronized.ref
    34     val error_fn: (output -> unit) Unsynchronized.ref
    35     val prompt_fn: (output -> unit) Unsynchronized.ref
    36     val status_fn: (output -> unit) Unsynchronized.ref
    37     val report_fn: (output -> unit) Unsynchronized.ref
    38     val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    39   end
    40   val urgent_message: string -> unit
    41   val error_msg: string -> unit
    42   val prompt: string -> unit
    43   val status: string -> unit
    44   val report: string -> unit
    45   val raw_message: Properties.T -> string -> unit
    46 end;
    47 
    48 structure Output: OUTPUT =
    49 struct
    50 
    51 (** print modes **)
    52 
    53 type output = string;  (*raw system output*)
    54 
    55 fun default_output s = (s, size s);
    56 fun default_escape (s: output) = s;
    57 
    58 local
    59   val default = {output = default_output, escape = default_escape};
    60   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
    61 in
    62   fun add_mode name output escape =
    63     Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
    64   fun get_mode () =
    65     the_default default
    66       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    67 end;
    68 
    69 fun output_width x = #output (get_mode ()) x;
    70 val output = #1 o output_width;
    71 
    72 fun escape x = #escape (get_mode ()) x;
    73 
    74 
    75 
    76 (** output channels **)
    77 
    78 (* raw output primitives -- not to be used in user-space *)
    79 
    80 fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    81 fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    82 
    83 fun raw_writeln "" = ()
    84   | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
    85 
    86 
    87 (* Isabelle output channels *)
    88 
    89 structure Private_Hooks =
    90 struct
    91   val writeln_fn = Unsynchronized.ref raw_writeln;
    92   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    93   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    94   val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    95   val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    96   val prompt_fn = Unsynchronized.ref raw_stdout;
    97   val status_fn = Unsynchronized.ref (fn _: output => ());
    98   val report_fn = Unsynchronized.ref (fn _: output => ());
    99   val raw_message_fn =
   100     Unsynchronized.ref
   101       (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
   102 end;
   103 
   104 fun writeln s = ! Private_Hooks.writeln_fn (output s);
   105 fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
   106 fun tracing s = ! Private_Hooks.tracing_fn (output s);
   107 fun warning s = ! Private_Hooks.warning_fn (output s);
   108 fun error_msg s = ! Private_Hooks.error_fn (output s);
   109 fun prompt s = ! Private_Hooks.prompt_fn (output s);
   110 fun status s = ! Private_Hooks.status_fn (output s);
   111 fun report s = ! Private_Hooks.report_fn (output s);
   112 fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
   113 
   114 fun legacy_feature s = warning ("Legacy feature! " ^ s);
   115 
   116 end;
   117 
   118 structure Basic_Output: BASIC_OUTPUT = Output;
   119 open Basic_Output;