src/Pure/General/print_mode.ML
author wenzelm
Tue Sep 18 18:05:37 2007 +0200 (2007-09-18)
changeset 24634 38db11874724
parent 24613 bc889c3d55a3
child 25118 158149a6e95b
permissions -rw-r--r--
simplified PrintMode interfaces;
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@24634
    19
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    20
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    21
end;
wenzelm@23934
    22
wenzelm@23827
    23
structure PrintMode: PRINT_MODE =
wenzelm@23827
    24
struct
wenzelm@23827
    25
wenzelm@23827
    26
val print_mode = ref ([]: string list);
wenzelm@24613
    27
wenzelm@24613
    28
fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
wenzelm@24613
    29
fun print_mode_active s = member (op =) (print_mode_value ()) s;
wenzelm@23827
    30
wenzelm@24634
    31
fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
wenzelm@24634
    32
fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
wenzelm@23934
    33
wenzelm@23827
    34
end;
wenzelm@23827
    35
wenzelm@23934
    36
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    37
open BasicPrintMode;