diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index edc485afe1..be0a11a256 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -67,8 +67,12 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_PRETERM false #endif -#ifndef LEAN_DEFAULT_PP_COMPACT_GOALS -#define LEAN_DEFAULT_PP_COMPACT_GOALS false +#ifndef LEAN_DEFAULT_PP_GOAL_COMPACT +#define LEAN_DEFAULT_PP_GOAL_COMPACT false +#endif + +#ifndef LEAN_DEFAULT_PP_GOAL_MAX_HYPS +#define LEAN_DEFAULT_PP_GOAL_MAX_HYPS 200 #endif #ifndef LEAN_DEFAULT_PP_ALL @@ -91,7 +95,8 @@ static name * g_pp_beta = nullptr; static name * g_pp_numerals = nullptr; static name * g_pp_abbreviations = nullptr; static name * g_pp_preterm = nullptr; -static name * g_pp_compact_goals = nullptr; +static name * g_pp_goal_compact = nullptr; +static name * g_pp_goal_max_hyps = nullptr; static name * g_pp_all = nullptr; static list * g_distinguishing_pp_options = nullptr; @@ -112,7 +117,9 @@ void initialize_pp_options() { g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_preterm = new name{"pp", "preterm"}; g_pp_all = new name{"pp", "all"}; - g_pp_compact_goals = new name{"pp", "compact_goals"}; + g_pp_goal_compact = new name{"pp", "goal", "compact"}; + g_pp_goal_max_hyps = new name{"pp", "goal", "max_hypotheses"}; + register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(pretty printer) maximum expression depth, after that it will use ellipsis"); register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, @@ -145,8 +152,10 @@ void initialize_pp_options() { "(pretty printer) display abbreviations (i.e., revert abbreviation expansion when pretty printing)"); register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); - register_bool_option(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS, + register_bool_option(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT, "(pretty printer) try to display goal in a single line when possible"); + register_unsigned_option(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS, + "(pretty printer) maximum number of hypotheses to be displayed"); register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, "(pretty printer) display coercions, implicit parameters, fully qualified names, universes, " "and disable abbreviations, beta reduction and notation during pretty printing"); @@ -178,7 +187,8 @@ void finalize_pp_options() { delete g_pp_purify_metavars; delete g_pp_purify_locals; delete g_pp_beta; - delete g_pp_compact_goals; + delete g_pp_goal_compact; + delete g_pp_goal_max_hyps; delete g_pp_all; delete g_distinguishing_pp_options; } @@ -211,7 +221,8 @@ bool get_pp_beta(options const & opts) { return opts.get_bool(*g_ bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); } bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } -bool get_pp_compact_goals(options const & opts) { return opts.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS); } +bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); } +unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); } bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); } list const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index beaa7946a8..dd8fa66041 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -35,7 +35,8 @@ bool get_pp_purify_locals(options const & opts); bool get_pp_numerals(options const & opts); bool get_pp_abbreviations(options const & opts); bool get_pp_preterm(options const & opts); -bool get_pp_compact_goals(options const & opts); +bool get_pp_goal_compact(options const & opts); +unsigned get_pp_goal_max_hyps(options const & opts); bool get_pp_all(options const & opts); list const & get_distinguishing_pp_options(); diff --git a/src/library/util.cpp b/src/library/util.cpp index 8b0029d4da..ef463c7265 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "kernel/error_msgs.h" @@ -918,11 +919,12 @@ format format_goal(formatter const & _fmt, buffer const & hyps, expr const formatter fmt = _fmt.update_options(opts); unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); - bool compact = get_pp_compact_goals(opts); + bool compact = get_pp_goal_compact(opts); + unsigned max_hs = get_pp_goal_max_hyps(opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); format r; - unsigned i = hyps.size(); - bool first = true; + unsigned i = std::min(max_hs, hyps.size()); + bool first = true; while (i > 0) { i--; expr l = hyps[i]; @@ -943,6 +945,8 @@ format format_goal(formatter const & _fmt, buffer const & hyps, expr const r = compose(comma(), line()) + r; r = group(ids + space() + colon() + nest(indent, line() + fmt(t))) + r; } + if (hyps.size() > max_hs) + r = r + compose(comma(), line()) + format("... (set pp.goal.max_hypotheses to display remaining hypotheses)"); if (compact) r = group(r); r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion)));