19 structure ML_Options: ML_OPTIONS = |
19 structure ML_Options: ML_OPTIONS = |
20 struct |
20 struct |
21 |
21 |
22 (* source trace *) |
22 (* source trace *) |
23 |
23 |
24 val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false); |
24 val source_trace_raw = |
|
25 Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false); |
25 val source_trace = Config.bool source_trace_raw; |
26 val source_trace = Config.bool source_trace_raw; |
26 |
27 |
27 |
28 |
28 (* exception trace *) |
29 (* exception trace *) |
29 |
30 |
30 val exception_trace_raw = Config.declare_option "ML_exception_trace"; |
31 val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here}); |
31 val exception_trace = Config.bool exception_trace_raw; |
32 val exception_trace = Config.bool exception_trace_raw; |
32 |
33 |
33 fun exception_trace_enabled NONE = |
34 fun exception_trace_enabled NONE = |
34 (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) |
35 (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) |
35 | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; |
36 | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; |
36 |
37 |
37 |
38 |
38 (* print depth *) |
39 (* print depth *) |
39 |
40 |
40 val print_depth_raw = |
41 val print_depth_raw = |
41 Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ())); |
42 Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ())); |
42 val print_depth = Config.int print_depth_raw; |
43 val print_depth = Config.int print_depth_raw; |
43 |
44 |
44 fun get_print_depth () = |
45 fun get_print_depth () = |
45 (case Context.thread_data () of |
46 (case Context.thread_data () of |
46 NONE => get_default_print_depth () |
47 NONE => get_default_print_depth () |