fix: refactor changes

src/Std/Internal/Http/Data/Headers/Basic.lean

@@ -228,7 +228,7 @@ structure Host where
   /--
   Optional port.
   -/
-  port : Option URI.Port
+  port : URI.Port
 deriving Repr, BEq
 
 namespace Host
@@ -247,8 +247,9 @@ Serializes a `Host` header back to a name and a value.
 -/
 def serialize (host : Host) : Header.Name × Header.Value :=
   let value := match host.port with
-    | some port => Header.Value.ofString! s!"{host.host}:{port}"
-    | none => Header.Value.ofString! <| toString host.host
+    | .value port => Header.Value.ofString! s!"{host.host}:{port}"
+    | .empty => Header.Value.ofString! s!"{host.host}:"
+    | .omitted => Header.Value.ofString! <| toString host.host
 
   (.mk "host", value)
 

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

@@ -295,8 +295,9 @@ private def authorityHostHeaderValue (authority : URI.Authority) : Header.Value
   let host := toString authority.host
 
   let value := match authority.port with
-    | some port => s!"{host}:{port}"
-    | none => host
+    | .value port => s!"{host}:{port}"
+    | .empty => s!"{host}:"
+    | .omitted => s!"{host}"
 
   Header.Value.ofString! value
 

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

@@ -89,7 +89,7 @@ Fails if the input starts with a non-token character or is empty.
 -/
 @[inline]
 def parseToken (limit : Nat) : Parser ByteSlice :=
-  takeWhileUpTo1 (fun c => token (Char.ofUInt8 c)) limit
+  takeWhileUpTo1 (fun c => tchar (Char.ofUInt8 c)) limit
 
 /--
 Parses a line terminator.