max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: formatter: escape identifiers

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-05 12:23:34 +02:00 • committed by Leonardo de Moura
parent c43e6624f9
commit eded953022
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -238,11 +238,20 @@ goLeft
def identNoAntiquot.formatter : Formatter | _ => do
checkKind identKind;
stx ← getCur;
-- TODO: pretty-print Name using «»
pushToken stx.getId.toString;
let s := stx.getId.toString;
-- try to parse `s` as-is; if it fails, escape
pst ← parseToken s;
let s := if pst.stxStack == #[stx] then s else match stx.getId with
| Name.str Name.anonymous s _ => "«" ++ s ++ "»"
| _ => panic! "unimplemented: escaping non-atomic identifiers (is anyone even using those?)";
pushToken s;
goLeft
@[builtinFormatter rawIdent] def rawIdent.formatter := identNoAntiquot.formatter
@[builtinFormatter rawIdent] def rawIdent.formatter : Formatter | _ => do
checkKind identKind;
stx ← getCur;
pushToken stx.getId.toString;
goLeft
def visitAtom (k : SyntaxNodeKind) : Formatter | p => do
stx ← getCur;