# HG changeset patch
# User wenzelm
# Date 1192899271 -7200
# Node ID 158149a6e95b322ca7d35646a9ac5ac8df690f0b
# Parent  74b279146ecbf3d6fd1fb444b024170ee38f898d
added input/internal, which are never active in print_mode_value;

diff -r 74b279146ecb -r 158149a6e95b src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Sat Oct 20 18:54:30 2007 +0200
+++ b/src/Pure/General/print_mode.ML	Sat Oct 20 18:54:31 2007 +0200
@@ -16,6 +16,8 @@
 signature PRINT_MODE =
 sig
   include BASIC_PRINT_MODE
+  val input: string
+  val internal: string
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
 end;
@@ -23,9 +25,13 @@
 structure PrintMode: PRINT_MODE =
 struct
 
-val print_mode = ref ([]: string list);
+val input = "input";
+val internal = "internal";
 
-fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
+val print_mode = ref ([]: string list);
+fun get_mode () = subtract (op =) [input, internal] (! print_mode);
+
+fun print_mode_value () = NAMED_CRITICAL "print_mode" get_mode;
 fun print_mode_active s = member (op =) (print_mode_value ()) s;
 
 fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);