From f03131610f701f84723b9e06cfb80176b747ce7d Mon Sep 17 00:00:00 2001 From: mehbark Date: Tue, 28 Jan 2025 20:57:29 -0500 Subject: [PATCH] streaming --- Main.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Main.lean b/Main.lean index 3e26416..ae58106 100644 --- a/Main.lean +++ b/Main.lean @@ -59,13 +59,17 @@ def main : List String → IO UInt32 | [width] => if let some width := width.toNat? then do - let mut text := "" let stdin ← IO.getStdin + let mut remainder : Array String := #[] while true do let line ← stdin.getLine if line.isEmpty then break - text := text ++ line - IO.println $ solve width text + let lines := breakUp width (remainder ++ line.words) + if h : lines.size > 0 then + remainder := lines[lines.size-1] + for line in lines[0:lines.size-1] do + IO.println $ justify width line + IO.println $ String.intercalate " " remainder.toList return 0 else fail | _ => fail