From 39f8fd8eb909f109479ca714687d0bd66fc0a4be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Sep 2020 16:58:23 -0700
Subject: [PATCH] fix: trailing ';' at end of input

---
 src/Lean/Parser/Do.lean             | 2 +-
 tests/lean/run/doTrailingAtEOI.lean | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/doTrailingAtEOI.lean

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 076c44ee54..83eaa4b682 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -78,7 +78,7 @@ withPosition fun pos₁ =>
     ("; "
      -- check indentation
      >> checkColGe pos₁.column "do-elements must be indented"
-     >> notFollowedByCommandToken)
+     >> notFollowedByCommandToken >> notFollowedBy eoi)
   >> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
diff --git a/tests/lean/run/doTrailingAtEOI.lean b/tests/lean/run/doTrailingAtEOI.lean
new file mode 100644
index 0000000000..c0b174749b
--- /dev/null
+++ b/tests/lean/run/doTrailingAtEOI.lean
@@ -0,0 +1,6 @@
+new_frontend
+
+
+def f (x : Nat) : IO Nat := do
+IO.println x;
+pure x;