feat: allow trailing ; at doSeqBracketed

src/Init/LeanInit.lean

@@ -781,6 +781,11 @@ def isAtom : Syntax → Bool
 | atom _ _ => true
 | _        => false
 
+def isToken (token : String) : Syntax → Bool
+| atom _ val => val.trim == token.trim
+| _          => false
+
+
 def isIdent : Syntax → Bool
 | ident _ _ _ _ => true
 | _             => false

src/Lean/Elab/Do.lean

@@ -43,7 +43,11 @@ match expectedType? with
 private def getDoElems (stx : Syntax) : Array Syntax :=
 let arg := stx.getArg 1;
 if arg.getKind == `Lean.Parser.Term.doSeqBracketed then
-  (arg.getArg 1).getArgs
+  let args := (arg.getArg 1).getArgs;
+  if args.back.isToken ";" then -- temporary hack
+    args.pop
+  else
+    args
 else
   arg.getArgs
 
@@ -219,6 +223,7 @@ fun stx expectedType? => do
   let doElems := getDoElems stx;
   trace `Elab.do $ fun _ => stx;
   let doElems := doElems.getSepElems;
+  trace `Elab.do $ fun _ => "doElems: " ++ toString doElems;
   { m := m, hasBindInst := bindInstVal, .. } ← extractBind expectedType?;
   result ← processDoElems doElems m bindInstVal expectedType?.get!;
   -- dbgTrace ("result: " ++ toString result);

src/Lean/Parser/Do.lean

@@ -22,7 +22,7 @@ def leftArrow : Parser := unicodeSymbol " ← " " <- "
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 
 def doSeqIndent    := withPosition fun pos => sepBy1 doElemParser (try ("; " >> checkColGe pos.column "do-elements must be indented"))
-def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " >> "}"
+def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 
 @[builtinDoElemParser] def doLet  := parser! "let " >> letDecl

tests/lean/run/doNotation1.lean

@@ -52,6 +52,13 @@ m1;
 m2 a;
 pure 1
 
+def tst0 : IO Unit := do {
+a ← f;
+let x := a + 1;
+IO.println "hello";
+IO.println x;
+}
+
 def tst1 : IO Unit := do
 a ← f;
 let x := a + 1;