# HG changeset patch
# User wenzelm
# Date 1184671179 -7200
# Node ID 0f0d1cf4992d4ca398a008138de0bdb32b28f016
# Parent  4639035739343f9be9a899ae57a64c86eada7803
Generic print mode.

diff -r 463903573934 -r 0f0d1cf4992d src/Pure/General/print_mode.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/print_mode.ML	Tue Jul 17 13:19:39 2007 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Pure/General/print_mode.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Generic print mode -- implicit configuration for various output
+mechanisms.
+*)
+
+signature PRINT_MODE =
+sig
+  val print_mode: string list ref
+  val print_mode_active: string -> bool
+end;
+
+structure PrintMode: PRINT_MODE =
+struct
+
+val print_mode = ref ([]: string list);
+fun print_mode_active s = member (op =) (! print_mode) s;
+
+end;
+
+open PrintMode;