src/Pure/General/print_mode.ML
author wenzelm
Sat Oct 20 18:54:31 2007 +0200 (2007-10-20 ago)
changeset 25118 158149a6e95b
parent 24634 38db11874724
child 25734 b00b903ae8ae
permissions -rw-r--r--
added input/internal, which are never active in print_mode_value;
wenzelm@23827
     1
(*  Title:      Pure/General/print_mode.ML
wenzelm@23827
     2
    ID:         $Id$
wenzelm@23827
     3
    Author:     Makarius
wenzelm@23827
     4
wenzelm@23827
     5
Generic print mode -- implicit configuration for various output
wenzelm@23827
     6
mechanisms.
wenzelm@23827
     7
*)
wenzelm@23827
     8
wenzelm@23934
     9
signature BASIC_PRINT_MODE =
wenzelm@23827
    10
sig
wenzelm@23827
    11
  val print_mode: string list ref
wenzelm@24613
    12
  val print_mode_value: unit -> string list
wenzelm@23827
    13
  val print_mode_active: string -> bool
wenzelm@23827
    14
end;
wenzelm@23827
    15
wenzelm@23934
    16
signature PRINT_MODE =
wenzelm@23934
    17
sig
wenzelm@23934
    18
  include BASIC_PRINT_MODE
wenzelm@25118
    19
  val input: string
wenzelm@25118
    20
  val internal: string
wenzelm@24634
    21
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    22
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    23
end;
wenzelm@23934
    24
wenzelm@23827
    25
structure PrintMode: PRINT_MODE =
wenzelm@23827
    26
struct
wenzelm@23827
    27
wenzelm@25118
    28
val input = "input";
wenzelm@25118
    29
val internal = "internal";
wenzelm@24613
    30
wenzelm@25118
    31
val print_mode = ref ([]: string list);
wenzelm@25118
    32
fun get_mode () = subtract (op =) [input, internal] (! print_mode);
wenzelm@25118
    33
wenzelm@25118
    34
fun print_mode_value () = NAMED_CRITICAL "print_mode" get_mode;
wenzelm@24613
    35
fun print_mode_active s = member (op =) (print_mode_value ()) s;
wenzelm@23827
    36
wenzelm@24634
    37
fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
wenzelm@24634
    38
fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
wenzelm@23934
    39
wenzelm@23827
    40
end;
wenzelm@23827
    41
wenzelm@23934
    42
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    43
open BasicPrintMode;