From 91b0dcad0f577bc1086afce1b487fc842f0e2e5c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Jul 2014 17:48:41 -0700
Subject: [PATCH] fix(library/tactic): avoid 'unknown' message in trace_tac
 when position information is not available

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/expr_to_tactic.cpp | 2 +-
 src/library/tactic/tactic.cpp         | 8 ++++++++
 src/library/tactic/tactic.h           | 1 +
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index 752fde92a..a702f18e4 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -186,7 +186,7 @@ static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr cons
         if (p)
             return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));
         else
-            return trace_state_tactic("unknown", mk_pair(0, 0));
+            return trace_state_tactic();
     });
 static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) {
         buffer<expr> args;
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 414720828..fb70d7a60 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -112,6 +112,14 @@ tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigne
         });
 }
 
+tactic trace_state_tactic() {
+    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
+            diagnostic(env, ios) << "proof state\n" << s << endl;
+            ios.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
 tactic suppress_trace(tactic const & t) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
             io_state new_ios(ios);
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 2872174f5..b9de389a1 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -53,6 +53,7 @@ tactic trace_tactic(sstream const & msg);
 tactic trace_tactic(std::string const & msg);
 /** \brief Return a tactic that just displays the input state in the diagnostic channel. */
 tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigned> const & pos);
+tactic trace_state_tactic();
 /** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
 tactic suppress_trace(tactic const & t);
 /** \brief Return a tactic that performs \c t1 followed by \c t2. */