feat: add optionalOrLinebreak parser combinator

see #1218

src/Lean/Parser/Basic.lean

@@ -1211,6 +1211,19 @@ def checkLinebreakBefore (errorMsg : String := "line break") : Parser := {
   fn   := checkLinebreakBeforeFn errorMsg
 }
 
+def optionalOrLinebreakFn (p : ParserFn) : ParserFn := fun c s =>
+  let prevLinebreak := !s.stxStack.isEmpty && checkTailLinebreak s.stxStack.back
+  let iniSz  := s.stackSize
+  let iniPos := s.pos
+  let s := p c s
+  let s := if s.hasError && s.pos == iniPos && prevLinebreak then s.restore iniSz iniPos else s
+  s.mkNode nullKind iniSz
+
+@[inline] def optionalOrLinebreakNoAntiquot (p : Parser) : Parser := {
+  info := optionaInfo p.info
+  fn   := optionalOrLinebreakFn p.fn
+}
+
 private def pickNonNone (stack : Array Syntax) : Syntax :=
   match stack.findRev? fun stx => !stx.isNone with
   | none => Syntax.missing
@@ -1221,7 +1234,7 @@ def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   if checkTailNoWs prev then s else s.mkError errorMsg
 
 def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
-  info := epsilonInfo,
+  info := epsilonInfo
   fn   := checkNoWsBeforeFn errorMsg
 }
 

src/Lean/Parser/Command.lean

@@ -60,7 +60,7 @@ def optDeclSig       := leading_parser many (ppSpace >> (Term.simpleBinderWithou
 def declValSimple    := leading_parser " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
 def declValEqns      := leading_parser Term.matchAltsWhereDecls
 def whereStructField := leading_parser Term.letDecl
-def whereStructInst  := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (whereStructField >> optional ";"))) >> optional Term.whereDecls
+def whereStructInst  := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (whereStructField >> optionalOrLinebreak ";"))) >> optional Term.whereDecls
 /-
   Remark: we should not use `Term.whereDecls` at `declVal` because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
   Issue #753 showns an example that fails to be parsed when we used `Term.whereDecls`.

src/Lean/Parser/Extra.lean

@@ -20,6 +20,9 @@ attribute [runBuiltinParserAttributeHooks]
 @[runBuiltinParserAttributeHooks] def optional (p : Parser) : Parser :=
   optionalNoAntiquot (withAntiquotSpliceAndSuffix `optional p (symbol "?"))
 
+@[runBuiltinParserAttributeHooks] def optionalOrLinebreak (p : Parser) : Parser :=
+  optionalOrLinebreakNoAntiquot p
+
 @[runBuiltinParserAttributeHooks] def many (p : Parser) : Parser :=
   manyNoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
 

src/Lean/Parser/Term.lean

@@ -60,7 +60,7 @@ namespace Term
   incorrect syntax when the full expression is `show $T by exact $e`. -/
 def byTactic' := leading_parser "by " >> Tactic.tacticSeq
 
-def optSemicolon (p : Parser) : Parser := ppDedent $ optional ";" >> ppLine >> p
+def optSemicolon (p : Parser) : Parser := ppDedent $ optionalOrLinebreak ";" >> ppLine >> p
 
 -- `checkPrec` necessary for the pretty printer
 @[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
@@ -222,7 +222,7 @@ def letRecDecls      := leading_parser sepBy1 letRecDecl ", "
 def «letrec» := leading_parser:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
 
 @[runBuiltinParserAttributeHooks]
-def whereDecls := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (letRecDecl >> optional ";")))
+def whereDecls := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (letRecDecl >> optionalOrLinebreak ";")))
 @[runBuiltinParserAttributeHooks]
 def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 

src/Lean/PrettyPrinter/Formatter.lean

@@ -433,6 +433,9 @@ def manyNoAntiquot.formatter (p : Formatter) : Formatter := do
 @[combinatorFormatter Lean.Parser.optionalNoAntiquot]
 def optionalNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p
 
+@[combinatorFormatter Lean.Parser.optionalOrLinebreakNoAntiquot]
+def optionalOrLinebreakNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p
+
 @[combinatorFormatter Lean.Parser.many1Unbox]
 def many1Unbox.formatter (p : Formatter) : Formatter := do
   let stx ← getCur

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -453,6 +453,10 @@ def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do
 def optionalNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
   visitArgs p
 
+@[combinatorParenthesizer Lean.Parser.optionalOrLinebreakNoAntiquot]
+def optionalOrLinebreakNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
+  visitArgs p
+
 @[combinatorParenthesizer Lean.Parser.sepByNoAntiquot]
 def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
   let stx ← getCur

tests/lean/optionalOrLinebreak.lean

@@ -0,0 +1,17 @@
+def f (y : Nat) :=
+  let x := 1x + y -- Error
+
+structure Point where
+ x : Nat
+ y : Nat
+deriving Repr
+
+def mkPoint1 (a : Nat) : Point where
+  x := 1y := a -- Error
+
+def mkPoint2 (a : Nat) : Point where
+  x := 1
+  y := a
+
+def mkPoint3 (a : Nat) : Point where
+  x := 1; y := a

tests/lean/optionalOrLinebreak.lean.expected.out

@@ -0,0 +1,2 @@
+optionalOrLinebreak.lean:2:12: error: expected ';'
+optionalOrLinebreak.lean:10:8: error: expected ';'

tests/lean/run/ofNat_class.lean

@@ -10,6 +10,7 @@ local macro "ofNat_class" Class:ident n:num : command =>
     ofNat := ‹$Class α›.1
 
   instance {α} [OfNat α (nat_lit $n)] : $Class α where
-    $field:ident := $n)
+    $field:ident := $n
+  )
 
 ofNat_class Zero 0