src/Pure/Tools/simplifier_trace.ML
author wenzelm
Thu Dec 12 22:38:25 2013 +0100 (2013-12-12)
changeset 54731 384ac33802b0
parent 54730 de2d99b459b3
child 55316 885500f4aa6a
permissions -rw-r--r--
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm@54730
     1
(*  Title:      Pure/Tools/simplifier_trace.ML
wenzelm@54730
     2
    Author:     Lars Hupel, TU Muenchen
wenzelm@54730
     3
wenzelm@54730
     4
Interactive Simplifier trace.
wenzelm@54730
     5
*)
wenzelm@54730
     6
wenzelm@54730
     7
signature SIMPLIFIER_TRACE =
wenzelm@54730
     8
sig
wenzelm@54730
     9
  val simp_trace_test: bool Config.T
wenzelm@54730
    10
end
wenzelm@54730
    11
wenzelm@54730
    12
structure Simplifier_Trace: SIMPLIFIER_TRACE =
wenzelm@54730
    13
struct
wenzelm@54730
    14
wenzelm@54730
    15
(* Simplifier trace operations *)
wenzelm@54730
    16
wenzelm@54730
    17
val simp_trace_test =
wenzelm@54730
    18
  Attrib.setup_config_bool @{binding simp_trace_test} (K false)
wenzelm@54730
    19
wenzelm@54730
    20
val _ = Theory.setup
wenzelm@54731
    21
  (Simplifier.set_trace_ops
wenzelm@54730
    22
   {trace_invoke = fn {depth, term} => fn ctxt =>
wenzelm@54730
    23
      (if Config.get ctxt simp_trace_test then
wenzelm@54730
    24
        tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
wenzelm@54730
    25
          Syntax.string_of_term ctxt term)
wenzelm@54730
    26
       else (); ctxt),
wenzelm@54730
    27
    trace_apply = fn args => fn ctxt => fn cont =>
wenzelm@54730
    28
      (if Config.get ctxt simp_trace_test then
wenzelm@54730
    29
        tracing ("Simplifier " ^ @{make_string} args)
wenzelm@54731
    30
       else (); cont ctxt)})
wenzelm@54730
    31
wenzelm@54730
    32
wenzelm@54730
    33
(* PIDE protocol *)
wenzelm@54730
    34
wenzelm@54730
    35
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
wenzelm@54730
    36
wenzelm@54730
    37
end
wenzelm@54730
    38