# HG changeset patch
# User wenzelm
# Date 1386880093 -3600
# Node ID de2d99b459b3fc334ba789721b7661e2a11fe811
# Parent  c5cd7a58cf2d41c3ba602a1e7227b52e686b94de
skeleton for Simplifier trace by Lars Hupel;

diff -r c5cd7a58cf2d -r de2d99b459b3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Dec 12 21:14:33 2013 +0100
+++ b/src/Pure/Pure.thy	Thu Dec 12 21:28:13 2013 +0100
@@ -107,6 +107,7 @@
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/proof_general_pure.ML"
+ML_file "Tools/simplifier_trace.ML"
 
 
 section {* Further content for the Pure theory *}
diff -r c5cd7a58cf2d -r de2d99b459b3 src/Pure/Tools/simplifier_trace.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/simplifier_trace.ML	Thu Dec 12 21:28:13 2013 +0100
@@ -0,0 +1,38 @@
+(*  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.map_theory_simpset (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
+
diff -r c5cd7a58cf2d -r de2d99b459b3 src/Pure/Tools/simplifier_trace.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/simplifier_trace.scala	Thu Dec 12 21:28:13 2013 +0100
@@ -0,0 +1,18 @@
+/*  Title:      Pure/Tools/simplifier_trace.scala
+    Author:     Lars Hupel, TU Muenchen
+
+Interactive Simplifier trace.
+*/
+
+package isabelle
+
+
+object Simplifier_Trace
+{
+  /* PIDE protocol */
+
+  class Handler extends Session.Protocol_Handler
+  {
+    val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean]
+  }
+}
diff -r c5cd7a58cf2d -r de2d99b459b3 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Dec 12 21:14:33 2013 +0100
+++ b/src/Pure/build-jars	Thu Dec 12 21:28:13 2013 +0100
@@ -78,6 +78,7 @@
   Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
+  Tools/simplifier_trace.scala
   Tools/sledgehammer_params.scala
   Tools/task_statistics.scala
   library.scala