WebSocket: On_Close called when user explicitly closes a web socket via AWS.Net.WebSocket.Registry.Close

[dsauvage]

Description
In AWS.Net.WebSocket.Close implementation, it is documented that

      --  When the user explicitly closes a web socket, we do not call
      --  On_Close (this is only called when the other end closes the socket)

However, when the user explicitly closes a web socket via AWS.Net.WebSocket.Registry.Close, On_Close is called

Patch
aws-net-websocket-registry.adb.patch.txt

Different behavior in AWS.Net.WebSocket.Registry.Close implementations
On another note, calling AWS.Net.WebSocket.Registry.Close(Socket : in out Object'Class; internally calls Socket.Shutdown while calling AWS.Net.WebSocket.Registry.Close(To : Recipient; does not. Any rational on why having different behaviour ?

[briot]

Hi David, I think this is the wrong patch.  In our code, we have a heavily patched version of websocket support (removing some race conditions), and I ended up removing the incorrect comment instead. It is convenient for users if On_Close is called systematically, since you then have a nice place where to do cleanups for instance.  I think at some point I had added an extra `Reason` parameter to indicate whether it was called as a result of the user calling Close or not, but I no longer have that in the code so perhaps I am imagining things here. Emmanuel (not an AWS maintainer, just another user)