src/Pure/General/output.ML
changeset 32738 15bb09ca0378
parent 31685 c124445a4b61
child 32966 5b21661fe618
     1.1 --- a/src/Pure/General/output.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/General/output.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -11,13 +11,13 @@
     1.4    val priority: string -> unit
     1.5    val tracing: string -> unit
     1.6    val warning: string -> unit
     1.7 -  val tolerate_legacy_features: bool ref
     1.8 +  val tolerate_legacy_features: bool Unsynchronized.ref
     1.9    val legacy_feature: string -> unit
    1.10    val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
    1.11    val timeit: (unit -> 'a) -> 'a
    1.12    val timeap: ('a -> 'b) -> 'a -> 'b
    1.13    val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    1.14 -  val timing: bool ref
    1.15 +  val timing: bool Unsynchronized.ref
    1.16  end;
    1.17  
    1.18  signature OUTPUT =
    1.19 @@ -32,18 +32,18 @@
    1.20    val std_output: output -> unit
    1.21    val std_error: output -> unit
    1.22    val writeln_default: output -> unit
    1.23 -  val writeln_fn: (output -> unit) ref
    1.24 -  val priority_fn: (output -> unit) ref
    1.25 -  val tracing_fn: (output -> unit) ref
    1.26 -  val warning_fn: (output -> unit) ref
    1.27 -  val error_fn: (output -> unit) ref
    1.28 -  val debug_fn: (output -> unit) ref
    1.29 -  val prompt_fn: (output -> unit) ref
    1.30 -  val status_fn: (output -> unit) ref
    1.31 +  val writeln_fn: (output -> unit) Unsynchronized.ref
    1.32 +  val priority_fn: (output -> unit) Unsynchronized.ref
    1.33 +  val tracing_fn: (output -> unit) Unsynchronized.ref
    1.34 +  val warning_fn: (output -> unit) Unsynchronized.ref
    1.35 +  val error_fn: (output -> unit) Unsynchronized.ref
    1.36 +  val debug_fn: (output -> unit) Unsynchronized.ref
    1.37 +  val prompt_fn: (output -> unit) Unsynchronized.ref
    1.38 +  val status_fn: (output -> unit) Unsynchronized.ref
    1.39    val error_msg: string -> unit
    1.40    val prompt: string -> unit
    1.41    val status: string -> unit
    1.42 -  val debugging: bool ref
    1.43 +  val debugging: bool Unsynchronized.ref
    1.44    val no_warnings: ('a -> 'b) -> 'a -> 'b
    1.45    val debug: (unit -> string) -> unit
    1.46  end;
    1.47 @@ -60,10 +60,10 @@
    1.48  
    1.49  local
    1.50    val default = {output = default_output, escape = default_escape};
    1.51 -  val modes = ref (Symtab.make [("", default)]);
    1.52 +  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
    1.53  in
    1.54    fun add_mode name output escape = CRITICAL (fn () =>
    1.55 -    change modes (Symtab.update_new (name, {output = output, escape = escape})));
    1.56 +    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
    1.57    fun get_mode () =
    1.58      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    1.59  end;
    1.60 @@ -91,14 +91,14 @@
    1.61  
    1.62  (* Isabelle output channels *)
    1.63  
    1.64 -val writeln_fn = ref writeln_default;
    1.65 -val priority_fn = ref (fn s => ! writeln_fn s);
    1.66 -val tracing_fn = ref (fn s => ! writeln_fn s);
    1.67 -val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
    1.68 -val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
    1.69 -val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
    1.70 -val prompt_fn = ref std_output;
    1.71 -val status_fn = ref (fn _: string => ());
    1.72 +val writeln_fn = Unsynchronized.ref writeln_default;
    1.73 +val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.74 +val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.75 +val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
    1.76 +val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
    1.77 +val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
    1.78 +val prompt_fn = Unsynchronized.ref std_output;
    1.79 +val status_fn = Unsynchronized.ref (fn _: string => ());
    1.80  
    1.81  fun writeln s = ! writeln_fn (output s);
    1.82  fun priority s = ! priority_fn (output s);
    1.83 @@ -108,13 +108,13 @@
    1.84  fun prompt s = ! prompt_fn (output s);
    1.85  fun status s = ! status_fn (output s);
    1.86  
    1.87 -val tolerate_legacy_features = ref true;
    1.88 +val tolerate_legacy_features = Unsynchronized.ref true;
    1.89  fun legacy_feature s =
    1.90    (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
    1.91  
    1.92  fun no_warnings f = setmp warning_fn (K ()) f;
    1.93  
    1.94 -val debugging = ref false;
    1.95 +val debugging = Unsynchronized.ref false;
    1.96  fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
    1.97  
    1.98  
    1.99 @@ -140,9 +140,9 @@
   1.100  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   1.101  
   1.102  (*global timing mode*)
   1.103 -val timing = ref false;
   1.104 +val timing = Unsynchronized.ref false;
   1.105  
   1.106  end;
   1.107  
   1.108 -structure BasicOutput: BASIC_OUTPUT = Output;
   1.109 -open BasicOutput;
   1.110 +structure Basic_Output: BASIC_OUTPUT = Output;
   1.111 +open Basic_Output;