Generic print mode.
authorwenzelm
Tue Jul 17 13:19:39 2007 +0200 (2007-07-17)
changeset 238270f0d1cf4992d
parent 23826 463903573934
child 23828 a8a3962f8eeb
Generic print mode.
src/Pure/General/print_mode.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/print_mode.ML	Tue Jul 17 13:19:39 2007 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      Pure/General/print_mode.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Generic print mode -- implicit configuration for various output
     1.9 +mechanisms.
    1.10 +*)
    1.11 +
    1.12 +signature PRINT_MODE =
    1.13 +sig
    1.14 +  val print_mode: string list ref
    1.15 +  val print_mode_active: string -> bool
    1.16 +end;
    1.17 +
    1.18 +structure PrintMode: PRINT_MODE =
    1.19 +struct
    1.20 +
    1.21 +val print_mode = ref ([]: string list);
    1.22 +fun print_mode_active s = member (op =) (! print_mode) s;
    1.23 +
    1.24 +end;
    1.25 +
    1.26 +open PrintMode;