chore: more robust empty line handling

leanprover-community · Nov 1, 2023 · 4a1196a · 4a1196a
1 parent 474db93
commit 4a1196a
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -210,10 +210,11 @@ open REPL
 
 /-- Get lines from stdin until a blank line is entered. -/
 partial def getLines : IO String := do
-  match (← (← IO.getStdin).getLine) with
-  | "" => pure ""
-  | "\n" => pure "\n"
-  | line => pure <| line ++ (← getLines)
+  let line ← (← IO.getStdin).getLine
+  return if line.trim.isEmpty then
+    line
+  else
+    line ++ (← getLines)
 
 instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
   toJson x := match x with