with_modes []: non-critical;
authorwenzelm
Mon, 20 Aug 2007 20:44:02 +0200
changeset 24362 a9fe7ed25fa4
parent 24361 52a14669f9e9
child 24363 c4dcc7408226
with_modes []: non-critical;
src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Mon Aug 20 20:44:01 2007 +0200
+++ b/src/Pure/General/print_mode.ML	Mon Aug 20 20:44:02 2007 +0200
@@ -25,8 +25,9 @@
 val print_mode = ref ([]: string list);
 fun print_mode_active s = member (op =) (! print_mode) s;
 
-fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
-  setmp print_mode (modes @ ! print_mode) f x);
+fun with_modes [] f x = f x
+  | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
+      setmp print_mode (modes @ ! print_mode) f x);
 
 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
   setmp print_mode [] f x);