equal
deleted
inserted
replaced
134 | msgs => cat_lines (map snd msgs)); |
134 | msgs => cat_lines (map snd msgs)); |
135 |
135 |
136 |
136 |
137 (** controlled execution **) |
137 (** controlled execution **) |
138 |
138 |
139 val exception_trace_raw = Config.declare_option "exception_trace"; |
139 val exception_trace_raw = Config.declare_option "ML_exception_trace"; |
140 val exception_trace = Config.bool exception_trace_raw; |
140 val exception_trace = Config.bool exception_trace_raw; |
141 |
141 |
142 fun exception_trace_enabled NONE = |
142 fun exception_trace_enabled NONE = |
143 (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) |
143 (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) |
144 | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; |
144 | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; |