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