# HG changeset patch
# User blanchet
# Date 1391182914 -3600
# Node ID 48a347b40629c6c2bb017916fbcb63a3405afc3b
# Parent  dcb36a2540bc13f0182fb2faf9942c52504beec0
better tracing + syntactically correct 'metis' calls

diff -r dcb36a2540bc -r 48a347b40629 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:26:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:41:54 2014 +0100
@@ -342,39 +342,49 @@
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
 
-        val (preplay_data as {overall_preplay_outcome, ...}, isar_proof) =
+        val string_of_isar_proof =
+          string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
+
+        val trace = false
+
+        val isar_proof =
           refute_graph
-(*
-          |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
-*)
+          |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
           |> redirect_graph axioms tainted bot
-(*
-          |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
-*)
+          |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
           |> isar_proof true params assms lems
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
-          |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
-                 preplay_timeout)
+
+        val preplay_data as {overall_preplay_outcome, ...} =
+          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
+            preplay_timeout isar_proof
+
+        fun trace_isar_proof label proof =
+          if trace then
+            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
+          else
+            ()
 
         val (play_outcome, isar_proof) =
           isar_proof
+          |> tap (trace_isar_proof "Original")
           |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
                preplay_data
+          |> tap (trace_isar_proof "Compressed")
           |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
+          |> tap (trace_isar_proof "Tried0")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (try0_isar ? minimize_isar_step_dependencies preplay_data)
+          |> tap (trace_isar_proof "Minimized")
           |> `overall_preplay_outcome
           ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
-
-        val isar_text =
-          string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
       in
-        (case isar_text of
+        (case string_of_isar_proof isar_proof of
           "" =>
           if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
           else ""
-        | _ =>
+        | isar_text =>
           let
             val msg =
               (if verbose then
diff -r dcb36a2540bc -r 48a347b40629 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:26:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:41:54 2014 +0100
@@ -204,7 +204,7 @@
       | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
 
     val using_facts = with_facts "" (enclose "using " " ")
-    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("by (" ^ meth) ")") ls ss
+    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("(" ^ meth ^ " ") ")") ls ss
 
     (* Local facts are always passed via "using", which affects "meson" and "metis". This is
        arguably stylistically superior, because it emphasises the structure of the proof. It is also