src/Pure/ML/ml_options.ML

avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;

(*  Title:      Pure/ML/ml_options.ML
    Author:     Makarius

ML configuration options.
*)

signature ML_OPTIONS =
sig
  val source_trace_raw: Config.raw
  val source_trace: bool Config.T
  val exception_trace_raw: Config.raw
  val exception_trace: bool Config.T
  val exception_trace_enabled: Context.generic option -> bool
  val exception_debugger_raw: Config.raw
  val exception_debugger: bool Config.T
  val exception_debugger_enabled: Context.generic option -> bool
  val debugger_raw: Config.raw
  val debugger: bool Config.T
  val debugger_enabled: Context.generic option -> bool
end;

structure ML_Options: ML_OPTIONS =
struct

(* source trace *)

val source_trace_raw =
  Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false);
val source_trace = Config.bool source_trace_raw;


(* exception trace *)

val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here});
val exception_trace = Config.bool exception_trace_raw;

fun exception_trace_enabled NONE =
      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;


(* exception debugger *)

val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", @{here});
val exception_debugger = Config.bool exception_debugger_raw;

fun exception_debugger_enabled NONE =
      (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
  | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;


(* debugger *)

val debugger_raw = Config.declare_option ("ML_debugger", @{here});
val debugger = Config.bool debugger_raw;

fun debugger_enabled NONE =
      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
  | debugger_enabled (SOME context) = Config.get_generic context debugger;

end;