chore(library/tactic/tactic_state): improve pp_goal

src/library/local_context.h

@@ -80,6 +80,9 @@ class local_context {
                        optional<expr> const & value, binder_info const & bi);
 public:
     local_context():m_next_idx(0) {}
+
+    bool empty() const { return m_idx2local_decl.empty(); }
+
     expr mk_local_decl(expr const & type, binder_info const & bi = binder_info());
     expr mk_local_decl(expr const & type, expr const & value);
     expr mk_local_decl(name const & ppn, expr const & type, binder_info const & bi = binder_info());

src/library/tactic/tactic_state.cpp

@@ -57,8 +57,10 @@ format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) con
     format r                   = lctx.pp(fmt);
     unsigned indent            = get_pp_indent(get_options());
     bool unicode               = get_pp_unicode(get_options());
+    if (!lctx.empty())
+        r += line();
     format turnstile           = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
-    r += line() + turnstile + space() + nest(indent, fmt(decl.get_type()));
+    r += turnstile + space() + nest(indent, fmt(decl.get_type()));
     if (get_pp_goal_compact(get_options()))
         r = group(r);
     return r;

tests/lean/run/meta_tac1.lean

@@ -2,12 +2,14 @@ set_option pp.all true
 
 open tactic name
 
+set_option pp.goal.compact true
+
 #tactic (∀ (p : Prop), p → p),
  do env ← get_env,
     trace "testing",
     return ()
 
-#tactic (∀ (p : Prop), p → p),
+#tactic (∀ (p : Prop), p → p → p),
  do d ← get_decl ("nat" <s> "add"),
     trace_expr (declaration.type d),
     trace "nat.rec type:",