feat: use ppLine

src/Lean/Parser/Command.lean

@@ -24,18 +24,18 @@ def commentBody : Parser :=
 @[combinatorParenthesizer commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinatorFormatter commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
-def docComment       := parser! "/--" >> commentBody
+def docComment       := parser! "/--" >> commentBody >> ppLine
 def «private»        := parser! "private "
 def «protected»      := parser! "protected "
 def visibility       := «private» <|> «protected»
 def «noncomputable»  := parser! "noncomputable "
 def «unsafe»         := parser! "unsafe "
 def «partial»        := parser! "partial "
-def declModifiers    := parser! optional docComment >> optional Term.«attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
+def declModifiers (inline : Bool) := parser! optional docComment >> optional (Term.«attributes» >> if inline then skip else ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
 def declId           := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
 def declSig          := parser! many Term.bracketedBinder >> Term.typeSpec
 def optDeclSig       := parser! many Term.bracketedBinder >> Term.optType
-def declValSimple    := parser! " := " >> termParser
+def declValSimple    := parser! " :=\n" >> termParser
 def declValEqns      := parser! Term.matchAlts false
 def declVal          := declValSimple <|> declValEqns
 def «abbrev»         := parser! "abbrev " >> declId >> optDeclSig >> declVal
@@ -46,20 +46,20 @@ def «instance»       := parser! "instance " >> optional declId >> declSig >> d
 def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
 def inferMod         := parser! try ("{" >> "}")
-def ctor             := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
+def ctor             := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
 def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> many ctor
 def classInductive   := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
-def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
-def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
-def structInstBinder     := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
-def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
-def structCtor           := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
+def structExplicitBinder := parser! try (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
+def structImplicitBinder := parser! try (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
+def structInstBinder     := parser! try (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
+def structFields         := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder))
+def structCtor           := parser! try (declModifiers true >> ident >> optional inferMod >> " :: ")
 def structureTk          := parser! "structure "
 def classTk              := parser! "class "
 def «extends»            := parser! " extends " >> sepBy1 termParser ", "
 def «structure»          := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
 @[builtinCommandParser] def declaration := parser!
-declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
+declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 
 @[builtinCommandParser] def «section»      := parser! "section " >> optional ident
 @[builtinCommandParser] def «namespace»    := parser! "namespace " >> ident

src/Lean/Parser/Module.lean

@@ -12,13 +12,13 @@ namespace Parser
 namespace Module
 def «prelude»  := parser! "prelude"
 def «import»   := parser! "import " >> optional "runtime" >> ident
-def header     := parser! optional «prelude» >> many «import»
+def header     := parser! optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine
 /--
   Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
   return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
   for it in order to auto-generate helpers such as the pretty printer. -/
 @[runParserAttributeHooks]
-def module     := parser! header >> many commandParser
+def module     := parser! header >> many (commandParser >> ppLine >> ppLine)
 
 def updateTokens (c : ParserContext) : ParserContext :=
 { c with

src/Lean/Parser/Term.lean

@@ -129,8 +129,8 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
 
 def matchAlts (optionalFirstBar := true) : Parser :=
 parser! withPosition $
-  (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "|")
+  ppLine >> (if optionalFirstBar then optional "| " else "| ") >>
+  sepBy1 matchAlt (ppLine >> checkColGe "alternatives must be indented" >> "|")
 
 def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser