feat: indented by

@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```

src/Lean/Parser/Tactic.lean

@@ -9,6 +9,9 @@ namespace Lean
 namespace Parser
 namespace Tactic
 
+def nonEmptySeq := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
+def seq         := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
+
 def underscoreFn : ParserFn :=
 fun c s =>
   let s   := symbolFn "_" c s;

src/Lean/Parser/Term.lean

@@ -19,8 +19,9 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
 categoryParser `tactic rbp
 
-def Tactic.seq : Parser         := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
-def Tactic.nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
+def Tactic.indentedNonEmptySeq : Parser :=
+node `Lean.Parser.Tactic.seq $ withPosition fun pos =>
+  sepBy1 tacticParser (try ("; " >>  checkColGe pos.column "tatic must be indented"))
 
 def darrow : Parser := " => "
 
@@ -84,7 +85,7 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq
+def binderTactic  := parser! try (" := " >> " by ") >> Tactic.indentedNonEmptySeq
 def binderDefault := parser! " := " >> termParser
 def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
 def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
@@ -116,7 +117,7 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
   sepBy1 termParser ", " >> darrow >> termParser
 
 def matchAlts (optionalFirstBar := true) : Parser :=
-parser! withPosition $ fun pos =>
+parser! withPosition fun pos =>
   (if optionalFirstBar then optional "| " else "| ") >>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 
@@ -159,7 +160,7 @@ def doId   := parser! try (ident >> optType >> leftArrow) >> termParser
 def doPat  := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
 def doExpr := parser! termParser
 def doElem := doLet <|> doId <|> doPat <|> doExpr
-def doSeq  := withPosition $ fun pos => sepBy1 doElem (try ("; " >> checkColGe pos.column "do-elements must be indented"))
+def doSeq  := withPosition fun pos => sepBy1 doElem (try ("; " >> checkColGe pos.column "do-elements must be indented"))
 def bracketedDoSeq := parser! "{" >> sepBy1 doElem "; " >> "}"
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 @[builtinTermParser] def «do»  := parser!:maxPrec "do " >> (bracketedDoSeq <|> doSeq)
@@ -241,7 +242,7 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
 @[builtinTermParser] def map         := tparser! infixR " <$> " 100
 
-@[builtinTermParser] def byTactic    := parser!:maxPrec "by " >> Tactic.nonEmptySeq
+@[builtinTermParser] def byTactic    := parser!:maxPrec "by " >> Tactic.indentedNonEmptySeq
 
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
 

tests/lean/run/newfrontend1.lean

@@ -108,12 +108,10 @@ by {
 }
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-by {
-  intros h1 _ h3;
-  traceState;
-  { refine! Eq.trans ?pre ?post;
-    (exact h1) <|> (exact y; exact h3; assumption) }
-}
+by intros h1 _ h3;
+   traceState;
+   { refine! Eq.trans ?pre ?post;
+   (exact h1) <|> (exact y; exact h3; assumption) }
 
 namespace Foo
   def Prod.mk := 1
@@ -337,3 +335,17 @@ macro_rules
 
 def tst4 : {α : Type} → {β : Type} → α → β → α × β :=
 function α β a b => (a, b)
+
+theorem simple20 (x y z : Nat) : y = z → x = x → x = y → x = z :=
+by intros h1 h2 h3;
+   try (clear x); -- should fail
+   clear h2;
+   traceState;
+   apply Eq.trans;
+   exact h3;
+   exact h1
+
+theorem simple21 (x y z : Nat) : y = z → x = x → y = x → x = z :=
+fun h1 _ h3 =>
+  have x = y from by apply Eq.symm; assumption;
+  Eq.trans this (by assumption)