michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/pp): pp inaccessible patterns

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-10 10:38:42 -07:00
parent e6db3ce584
commit 299fd5c919
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/pp.cpp
View file

@ -29,6 +29,7 @@ Author: Leonardo de Moura
#include "library/pp_options.h"
#include "library/constants.h"
#include "library/replace_visitor.h"
#include "library/definitional/equations.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"
#include "frontends/lean/token_table.h"
@ -672,6 +673,10 @@ auto pretty_fn::pp_explicit(expr const & e) -> result {
auto pretty_fn::pp_macro(expr const & e) -> result {
if (is_explicit(e)) {
return pp_explicit(e);
} else if (is_inaccessible(e)) {
format li = m_unicode ? format("⌞") : format("?(");
format ri = m_unicode ? format("⌟") : format(")");
return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri)));
} else if (is_annotation(e)) {
return pp(get_annotation_arg(e));
} else {