1(* Title: Pure/ML/ml_options.ML 2 Author: Makarius 3 4ML configuration options. 5*) 6 7signature ML_OPTIONS = 8sig 9 val source_trace_raw: Config.raw 10 val source_trace: bool Config.T 11 val exception_trace_raw: Config.raw 12 val exception_trace: bool Config.T 13 val exception_trace_enabled: Context.generic option -> bool 14 val exception_debugger_raw: Config.raw 15 val exception_debugger: bool Config.T 16 val exception_debugger_enabled: Context.generic option -> bool 17 val debugger_raw: Config.raw 18 val debugger: bool Config.T 19 val debugger_enabled: Context.generic option -> bool 20end; 21 22structure ML_Options: ML_OPTIONS = 23struct 24 25(* source trace *) 26 27val source_trace_raw = 28 Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false); 29val source_trace = Config.bool source_trace_raw; 30 31 32(* exception trace *) 33 34val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>); 35val exception_trace = Config.bool exception_trace_raw; 36 37fun exception_trace_enabled NONE = 38 (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) 39 | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; 40 41 42(* exception debugger *) 43 44val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>); 45val exception_debugger = Config.bool exception_debugger_raw; 46 47fun exception_debugger_enabled NONE = 48 (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false) 49 | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger; 50 51 52(* debugger *) 53 54val debugger_raw = Config.declare_option ("ML_debugger", \<^here>); 55val debugger = Config.bool debugger_raw; 56 57fun debugger_enabled NONE = 58 (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false) 59 | debugger_enabled (SOME context) = Config.get_generic context debugger; 60 61end; 62