fix: comments

Author: algebraic-dev

src/Std/Internal/Http/Data/Body.lean

@@ -45,9 +45,6 @@ deriving Inhabited
 
 namespace Body
 
-instance : EmptyCollection Body where
-  emptyCollection := Body.zero
-
 /--
 Get content length of a body (if known).
 -/
@@ -75,6 +72,9 @@ instance : Coe ByteArray Body where
 instance : Coe Body.ByteStream Body where
   coe := .stream
 
+instance : EmptyCollection Body where
+  emptyCollection := Body.zero
+
 instance : ForIn Async Body Chunk where
   forIn body acc step :=
     match body with

src/Std/Internal/Http/Data/Body/ByteStream.lean

@@ -9,7 +9,6 @@ prelude
 public import Std.Sync
 public import Init.Data.Vector
 public import Std.Internal.Async
-public import Std.Internal.Async.IO
 public import Std.Internal.Http.Internal
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Body.Length
@@ -19,9 +18,9 @@ public section
 /-!
 # ByteStream
 
-This module defines the `ByteStream` structure, which represents a channel for reading and
-writing sequences of bytes. It provides utilities for efficiently processing byte arrays
-in a streaming fashion, including support for chunk extensions.
+A `ByteStream` represents an asynchronous channel for streaming byte data in chunks. It provides an
+interface for producers and consumers to exchange byte arrays with optional chunk metadata (extensions),
+aking it suitable for HTTP chunked transfer encoding and other streaming scenarios.
 -/
 
 namespace Std.Http.Body
@@ -55,16 +54,14 @@ def empty : Async ByteStream :=
   emptyWithCapacity
 
 /--
-Tries to receive a chunk from the stream.
-Returns `some` with a chunk when data is available, or `none` when the stream is closed
-or no data is available.
+Tries to receive a chunk from the stream. Returns `some` with a chunk when data is available, or `none`
+hen the stream is closed or no data is available.
 -/
 def tryRecv (stream : ByteStream) : Async (Option Chunk) := do
   stream.channel.tryRecv
 
 /--
-Receives (reads) a chunk from the stream.
-Returns `none` if the stream is closed and no data is available.
+Receives (reads) a chunk from the stream. Returns `none` if the stream is closed and no data is available.
 -/
 def recv (stream : ByteStream) : Async (Option Chunk) := do
   let task ← stream.channel.recv

src/Std/Internal/Http/Protocol/H1.lean

@@ -551,7 +551,7 @@ partial def processRead (machine : Machine dir) : Machine dir :=
           machine
 
   | .needChunkedBody ext 0 =>
-    let (machine, result) := parseWith machine (parseLastChunkBody machine.config) (limit := some 1)
+    let (machine, result) := parseWith machine (parseLastChunkBody machine.config) (limit := some 2)
 
     match result with
     | some _ =>

src/Std/Internal/Http/Server/Connection.lean

@@ -240,14 +240,8 @@ private def handle
           machine := machine.setKnownSize (size.getD .chunked)
           respStream := some stream
 
-  let (_, output) := machine.takeOutput
-
-  if output.size > 0 then
-    Transport.sendAll socket output.data
-
   if let some res := respStream then
-    if ¬ (← res.isClosed) then
-      res.close
+    if ¬ (← res.isClosed) then res.close
 
 end Connection