equal
deleted
inserted
replaced
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; |