src/Pure/General/print_mode.ML
author wenzelm
Mon, 17 Sep 2007 16:36:43 +0200
changeset 24613 bc889c3d55a3
parent 24603 425d6445cba6
child 24634 38db11874724
permissions -rw-r--r--
added print_mode_value (CRITICAL);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/print_mode.ML
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     4
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     5
Generic print mode -- implicit configuration for various output
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     6
mechanisms.
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     7
*)
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
     8
23934
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
     9
signature BASIC_PRINT_MODE =
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    10
sig
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    11
  val print_mode: string list ref
24613
bc889c3d55a3 added print_mode_value (CRITICAL);
wenzelm
parents: 24603
diff changeset
    12
  val print_mode_value: unit -> string list
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    13
  val print_mode_active: string -> bool
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    14
end;
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    15
23934
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    16
signature PRINT_MODE =
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    17
sig
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    18
  include BASIC_PRINT_MODE
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    19
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    20
  val with_default: ('a -> 'b) -> 'a -> 'b
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    21
end;
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    22
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    23
structure PrintMode: PRINT_MODE =
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    24
struct
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    25
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    26
val print_mode = ref ([]: string list);
24613
bc889c3d55a3 added print_mode_value (CRITICAL);
wenzelm
parents: 24603
diff changeset
    27
bc889c3d55a3 added print_mode_value (CRITICAL);
wenzelm
parents: 24603
diff changeset
    28
fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
bc889c3d55a3 added print_mode_value (CRITICAL);
wenzelm
parents: 24603
diff changeset
    29
fun print_mode_active s = member (op =) (print_mode_value ()) s;
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    30
24603
425d6445cba6 with_modes: always CRITICAL;
wenzelm
parents: 24362
diff changeset
    31
fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
425d6445cba6 with_modes: always CRITICAL;
wenzelm
parents: 24362
diff changeset
    32
  setmp print_mode (modes @ ! print_mode) f x);
23934
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    33
24058
81aafd465662 NAMED_CRITICAL;
wenzelm
parents: 23934
diff changeset
    34
fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
81aafd465662 NAMED_CRITICAL;
wenzelm
parents: 23934
diff changeset
    35
  setmp print_mode [] f x);
23934
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    36
23827
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    37
end;
0f0d1cf4992d Generic print mode.
wenzelm
parents:
diff changeset
    38
23934
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    39
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
79393cb9c0a6 added with_modes, with_default;
wenzelm
parents: 23827
diff changeset
    40
open BasicPrintMode;