From 46d05d926ea31c2e9fad8c01e51cf928c1bffe11 Mon Sep 17 00:00:00 2001 From: Yifan Luo Date: Thu, 9 Nov 2023 17:05:25 +0100 Subject: [PATCH] more --- index.src.html | 37 +++++++++++++------------------------ 1 file changed, 13 insertions(+), 24 deletions(-) diff --git a/index.src.html b/index.src.html index a2721dc..b9543a4 100644 --- a/index.src.html +++ b/index.src.html @@ -339,6 +339,11 @@

Framework

IP Address Space

+ Define {{IPAddressSpace}} as follows: +
+    enum IPAddressSpace { "public","private", "local" };
+  
+ Every IP address belongs to an IP address space, which can be one of three different values: @@ -963,10 +968,6 @@

Fetch API

The Fetch API needs to be adjusted as well. - - Define {{IPAddressSpace}} as follows. -
-        enum IPAddressSpace { "public","private", "local" };
-      
- Append an optional [=map/entry=] to {{RequestInfo}}, whose [=map/key=] is targetAddressSpace, and [=map/value=] is a {{IPAddressSpace}}. @@ -975,26 +976,14 @@

Fetch API

IPAddressSpace targetAddressSpace; }; - - The new - Request(input, |init|) is - appended with the following step right before setting [=this=]'s [=request=] - to |request|: - 1. If |init|["{{RequestInit/targetAddressSpace}}"] [=map/exists=], and - |request|'s [=request/client=] is a [=secure context=], then switch on - |init|["{{RequestInit/targetAddressSpace}}"]: -
-
public -
Set |request|'s [=target IP address space=] to [=IP address - space/public=] - -
private -
Set |request|'s [=target IP address space=] to [=IP address - space/private=]. - -
local -
Set |request|'s [=target IP address space=] to [=IP address - space/local=] -
+ + - Define a new targetAddressSpace representing the + above in [=request=]. +
+        partial interface Request {
+          readonly attribute IPAddressSpace targetAddressSpace;
+        };
+      

Forbidden header names