diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 8effd2c7c9..53377e6b6c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2029,7 +2029,7 @@ void parser::parse_command() {
         lazy_type_context tc(m_env, get_options());
         scope_global_ios scope1(m_ios);
         scope_trace_env  scope2(m_env, m_ios.get_options(), tc);
-        scope_traces_as_messages traces_as_messages(get_file_name(), pos());
+        scope_traces_as_messages traces_as_messages(get_stream_name(), pos());
         if (is_notation_cmd(cmd_name)) {
             in_notation_ctx ctx(*this);
             if (it->get_skip_token())
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index 106cc65e70..2b7a4e1eae 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include <string>
 #include "util/sexpr/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
@@ -218,7 +219,7 @@ void finalize_trace() {
     delete g_trace_as_messages;
 }
 
-scope_traces_as_messages::scope_traces_as_messages(char const * stream_name, pos_info const & pos) :
+scope_traces_as_messages::scope_traces_as_messages(std::string const & stream_name, pos_info const & pos) :
         m_stream_name(stream_name), m_pos(pos) {
     if (get_global_ios().get_options().get_bool(*g_trace_as_messages, false)) {
         m_redirected_ios = std::unique_ptr<io_state>(new io_state(get_global_ios()));
@@ -231,7 +232,7 @@ scope_traces_as_messages::scope_traces_as_messages(char const * stream_name, pos
 
 scope_traces_as_messages::scope_traces_as_messages(pos_info_provider const *provider, expr const &ref) :
     scope_traces_as_messages(provider ? provider->get_file_name() : "<unknown>",
-                             provider ? provider->get_pos_info_or_some(ref) : pos_info(0, 0)) {}
+                             provider ? provider->get_pos_info_or_some(ref) : pos_info(1, 0)) {}
 
 scope_traces_as_messages::~scope_traces_as_messages() {
     if (enabled()) {
diff --git a/src/library/trace.h b/src/library/trace.h
index f1b9ecb7ed..4f59c1b9b4 100644
--- a/src/library/trace.h
+++ b/src/library/trace.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
+#include <string>
 #include "library/io_state_stream.h"
 
 namespace lean {
@@ -31,14 +32,14 @@ public:
 };
 
 class scope_traces_as_messages {
-    char const *                           m_stream_name;
+    std::string                            m_stream_name;
     pos_info                               m_pos;
     std::unique_ptr<io_state>              m_redirected_ios;
     std::unique_ptr<scope_global_ios>      m_scoped_ios;
     std::shared_ptr<string_output_channel> m_buffer;
 
 public:
-    scope_traces_as_messages(char const * stream_name, pos_info const & pos);
+    scope_traces_as_messages(std::string const & stream_name, pos_info const & pos);
     scope_traces_as_messages(pos_info_provider const * provider, expr const & ref);
     ~scope_traces_as_messages();
     bool enabled() const { return static_cast<bool>(m_scoped_ios); }