src/Pure/Tools/simplifier_trace.ML

clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;

(*  Title:      Pure/Tools/simplifier_trace.ML
    Author:     Lars Hupel, TU Muenchen

Interactive Simplifier trace.
*)

signature SIMPLIFIER_TRACE =
sig
  val simp_trace_test: bool Config.T
end

structure Simplifier_Trace: SIMPLIFIER_TRACE =
struct

(* Simplifier trace operations *)

val simp_trace_test =
  Attrib.setup_config_bool @{binding simp_trace_test} (K false)

val _ = Theory.setup
  (Simplifier.set_trace_ops
   {trace_invoke = fn {depth, term} => fn ctxt =>
      (if Config.get ctxt simp_trace_test then
        tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
          Syntax.string_of_term ctxt term)
       else (); ctxt),
    trace_apply = fn args => fn ctxt => fn cont =>
      (if Config.get ctxt simp_trace_test then
        tracing ("Simplifier " ^ @{make_string} args)
       else (); cont ctxt)})


(* PIDE protocol *)

val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"

end