From 42e681a5a6f28d7a41b92a1cf3b8aba56a5cab55 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 22 Jul 2021 15:21:28 +0200
Subject: [PATCH] fix: make unterminated comments consume all input

Fixes #549
---
 src/Lean/Parser/Basic.lean                               | 5 ++---
 src/Lean/Parser/Term.lean                                | 2 +-
 tests/lean/interactive/unterminatedDocComment.lean       | 9 +++++++++
 .../interactive/unterminatedDocComment.lean.expected.out | 6 ++++++
 tests/lean/tokenErrors.lean.expected.out                 | 5 +----
 5 files changed, 19 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/interactive/unterminatedDocComment.lean
 create mode 100644 tests/lean/interactive/unterminatedDocComment.lean.expected.out

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 6683bcb568..6f9faef7c6 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -724,7 +724,6 @@ def takeWhileFn (p : Char → Bool) : ParserFn :=
 @[inline] def takeWhile1Fn (p : Char → Bool) (errorMsg : String) : ParserFn :=
   andthenFn (satisfyFn p errorMsg) (takeWhileFn p)
 
-variable (startPos : String.Pos) in
 partial def finishCommentBlock (nesting : Nat) : ParserFn := fun c s =>
   let input := c.input
   let i     := s.pos
@@ -749,7 +748,7 @@ partial def finishCommentBlock (nesting : Nat) : ParserFn := fun c s =>
         else finishCommentBlock nesting c (s.setPos i)
     else finishCommentBlock nesting c (s.setPos i)
 where
-  eoi s := s.mkUnexpectedErrorAt "unterminated comment" startPos
+  eoi s := s.mkUnexpectedError "unterminated comment"
 
 /- Consume whitespace and comments -/
 partial def whitespace : ParserFn := fun c s =>
@@ -774,7 +773,7 @@ partial def whitespace : ParserFn := fun c s =>
         let i    := input.next i
         let curr := input.get i
         if curr == '-' then s -- "/--" doc comment is an actual token
-        else andthenFn (finishCommentBlock startPos 1) whitespace c (s.next input i)
+        else andthenFn (finishCommentBlock 1) whitespace c (s.next input i)
       else s
     else s
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 559e4aeb8e..187675d6d2 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -11,7 +11,7 @@ namespace Parser
 
 namespace Command
 def commentBody : Parser :=
-{ fn := rawFn (fun c s => finishCommentBlock s.pos 1 c s) (trailingWs := true) }
+{ fn := rawFn (finishCommentBlock 1) (trailingWs := true) }
 
 @[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
diff --git a/tests/lean/interactive/unterminatedDocComment.lean b/tests/lean/interactive/unterminatedDocComment.lean
new file mode 100644
index 0000000000..d8c5cc5bc5
--- /dev/null
+++ b/tests/lean/interactive/unterminatedDocComment.lean
@@ -0,0 +1,9 @@
+/--
+def a1 := sorry
+def a2 := sorry
+def a3 := sorry
+...
+ -
+--^ insert: /
+--^ collectDiagnostics
+def a4 := 0
diff --git a/tests/lean/interactive/unterminatedDocComment.lean.expected.out b/tests/lean/interactive/unterminatedDocComment.lean.expected.out
new file mode 100644
index 0000000000..7d543ec027
--- /dev/null
+++ b/tests/lean/interactive/unterminatedDocComment.lean.expected.out
@@ -0,0 +1,6 @@
+{"textDocument": {"version": 2, "uri": "file://unterminatedDocComment.lean"},
+ "contentChanges":
+ [{"text": "/",
+   "range":
+   {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 3}}}]}
+{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []}
diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out
index 027a00858f..737f2d0e4b 100644
--- a/tests/lean/tokenErrors.lean.expected.out
+++ b/tests/lean/tokenErrors.lean.expected.out
@@ -2,7 +2,4 @@ tokenErrors.lean:1:10: error: missing end of character literal
 tokenErrors.lean:2:9: error: invalid escape sequence
 tokenErrors.lean:3:7: error: unterminated string literal
 tokenErrors.lean:4:11: error: unterminated identifier escape
-tokenErrors.lean:6:0: error: unterminated comment
-tokenErrors.lean:7:0: error: unterminated comment
-tokenErrors.lean:7:1: error: unterminated comment
-tokenErrors.lean:7:0-7:1: error: unexpected command
+tokenErrors.lean:8:0: error: unterminated comment