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