src/Pure/General/print_mode.ML
changeset 24058 81aafd465662
parent 23934 79393cb9c0a6
child 24362 a9fe7ed25fa4
     1.1 --- a/src/Pure/General/print_mode.ML	Sun Jul 29 16:00:06 2007 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Sun Jul 29 17:28:55 2007 +0200
     1.3 @@ -25,10 +25,11 @@
     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 = CRITICAL (fn () =>
     1.8 +fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
     1.9    setmp print_mode (modes @ ! print_mode) f x);
    1.10  
    1.11 -fun with_default f x = setmp print_mode [] f x;
    1.12 +fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    1.13 +  setmp print_mode [] f x);
    1.14  
    1.15  end;
    1.16