src/Pure/General/print_mode.ML
changeset 25798 1e6eafbb466f
parent 25734 b00b903ae8ae
child 28122 3d099ce624e7
equal deleted inserted replaced
25797:b293e3ed3cad 25798:1e6eafbb466f
    40   in subtract (op =) [input, internal] modes end;
    40   in subtract (op =) [input, internal] modes end;
    41 
    41 
    42 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    42 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    43 
    43 
    44 fun setmp modes f x =
    44 fun setmp modes f x =
    45   let
    45   let val orig_modes = (case Multithreading.get_data tag of SOME (SOME ms) => SOME ms | _ => NONE)
    46     val orig_data =
    46   in setmp_thread_data tag orig_modes (SOME modes) f x end;
    47       (case Multithreading.get_data tag of
       
    48         SOME (SOME orig_modes) => SOME orig_modes
       
    49       | _ => NONE);
       
    50     val _ = Multithreading.put_data (tag, SOME modes);
       
    51     val result = Exn.capture f x;
       
    52     val _ = Multithreading.put_data (tag, orig_data);
       
    53   in Exn.release result end;
       
    54 
    47 
    55 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    48 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    56 fun closure f = with_modes [] f;
    49 fun closure f = with_modes [] f;
    57 
    50 
    58 end;
    51 end;