From 88164a5e91d53c005f7da55e894dd60997623939 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 2 Oct 2020 17:40:18 +0200
Subject: [PATCH] feat: more pp tweaks

---
 src/Lean/Parser/Command.lean | 4 ++--
 src/Lean/Parser/Term.lean    | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index f2f5fc5986..dbb2d9d0c7 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -64,8 +64,8 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
 @[builtinCommandParser] def «section»      := parser! "section " >> optional ident
 @[builtinCommandParser] def «namespace»    := parser! "namespace " >> ident
 @[builtinCommandParser] def «end»          := parser! "end " >> optional ident
-@[builtinCommandParser] def «variable»     := parser! "variable " >> Term.bracketedBinder
-@[builtinCommandParser] def «variables»    := parser! "variables " >> many1 Term.bracketedBinder
+@[builtinCommandParser] def «variable»     := parser! "variable" >> Term.bracketedBinder
+@[builtinCommandParser] def «variables»    := parser! "variables" >> many1 Term.bracketedBinder
 @[builtinCommandParser] def «universe»     := parser! "universe " >> ident
 @[builtinCommandParser] def «universes»    := parser! "universes " >> many1 ident
 @[builtinCommandParser] def check          := parser! "#check " >> termParser
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4572bc76a9..8f20443352 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -124,8 +124,8 @@ def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
 
 def matchAlt : Parser :=
-nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
-  sepBy1 termParser ", " >> darrow >> termParser
+nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ ppGroup $
+  ppGroup (sepBy1 termParser ", " >> darrow) >> termParser
 
 def matchAlts (optionalFirstBar := true) : Parser :=
 parser! withPosition $
@@ -161,7 +161,7 @@ def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
 @[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optional ";\n" >> termParser
 def attrArg : Parser := ident <|> strLit <|> numLit
 -- use `rawIdent` because of attribute names such as `instance`
-def attrInstance     := parser! rawIdent >> many (ppSpace >> attrArg)
+def attrInstance     := ppGroup $ parser! rawIdent >> many (ppSpace >> attrArg)
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 def letRecDecls      := sepBy1 (group (optional «attributes» >> letDecl)) ", "
 @[builtinTermParser] def «letrec» :=