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;
     1 (*  Title:      Pure/ML/ml_options.ML
     2     Author:     Makarius
     3 
     4 ML configuration options.
     5 *)
     6 
     7 signature ML_OPTIONS =
     8 sig
     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
    20 end;
    21 
    22 structure ML_Options: ML_OPTIONS =
    23 struct
    24 
    25 (* source trace *)
    26 
    27 val source_trace_raw =
    28   Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false);
    29 val source_trace = Config.bool source_trace_raw;
    30 
    31 
    32 (* exception trace *)
    33 
    34 val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>);
    35 val exception_trace = Config.bool exception_trace_raw;
    36 
    37 fun 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 
    44 val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>);
    45 val exception_debugger = Config.bool exception_debugger_raw;
    46 
    47 fun 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 
    54 val debugger_raw = Config.declare_option ("ML_debugger", \<^here>);
    55 val debugger = Config.bool debugger_raw;
    56 
    57 fun 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 
    61 end;