src/Pure/ML/ml_options.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69575 f77cc54f6d47
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@56303
     1
(*  Title:      Pure/ML/ml_options.ML
wenzelm@56303
     2
    Author:     Makarius
wenzelm@56303
     3
wenzelm@56303
     4
ML configuration options.
wenzelm@56303
     5
*)
wenzelm@56303
     6
wenzelm@56303
     7
signature ML_OPTIONS =
wenzelm@56303
     8
sig
wenzelm@56303
     9
  val source_trace_raw: Config.raw
wenzelm@56303
    10
  val source_trace: bool Config.T
wenzelm@56303
    11
  val exception_trace_raw: Config.raw
wenzelm@56303
    12
  val exception_trace: bool Config.T
wenzelm@56303
    13
  val exception_trace_enabled: Context.generic option -> bool
wenzelm@62498
    14
  val exception_debugger_raw: Config.raw
wenzelm@62498
    15
  val exception_debugger: bool Config.T
wenzelm@62498
    16
  val exception_debugger_enabled: Context.generic option -> bool
wenzelm@60730
    17
  val debugger_raw: Config.raw
wenzelm@60730
    18
  val debugger: bool Config.T
wenzelm@60730
    19
  val debugger_enabled: Context.generic option -> bool
wenzelm@56303
    20
end;
wenzelm@56303
    21
wenzelm@56303
    22
structure ML_Options: ML_OPTIONS =
wenzelm@56303
    23
struct
wenzelm@56303
    24
wenzelm@56303
    25
(* source trace *)
wenzelm@56303
    26
wenzelm@56438
    27
val source_trace_raw =
wenzelm@64556
    28
  Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false);
wenzelm@56303
    29
val source_trace = Config.bool source_trace_raw;
wenzelm@56303
    30
wenzelm@56303
    31
wenzelm@56303
    32
(* exception trace *)
wenzelm@56303
    33
wenzelm@64556
    34
val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>);
wenzelm@56303
    35
val exception_trace = Config.bool exception_trace_raw;
wenzelm@56303
    36
wenzelm@56303
    37
fun exception_trace_enabled NONE =
wenzelm@56303
    38
      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
wenzelm@56303
    39
  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
wenzelm@56303
    40
wenzelm@56303
    41
wenzelm@62498
    42
(* exception debugger *)
wenzelm@62498
    43
wenzelm@64556
    44
val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>);
wenzelm@62498
    45
val exception_debugger = Config.bool exception_debugger_raw;
wenzelm@62498
    46
wenzelm@62498
    47
fun exception_debugger_enabled NONE =
wenzelm@62498
    48
      (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
wenzelm@62498
    49
  | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;
wenzelm@62498
    50
wenzelm@62498
    51
wenzelm@60730
    52
(* debugger *)
wenzelm@60730
    53
wenzelm@64556
    54
val debugger_raw = Config.declare_option ("ML_debugger", \<^here>);
wenzelm@60730
    55
val debugger = Config.bool debugger_raw;
wenzelm@60730
    56
wenzelm@60730
    57
fun debugger_enabled NONE =
wenzelm@60730
    58
      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
wenzelm@60730
    59
  | debugger_enabled (SOME context) = Config.get_generic context debugger;
wenzelm@60730
    60
wenzelm@56303
    61
end;