From 77699754975693d7692cf4e7e7341710f017f9a0 Mon Sep 17 00:00:00 2001 From: totoro Date: Fri, 22 May 2015 23:54:33 +0200 Subject: [PATCH] add to_List_String of HTTP_Header. This format the list of the couple Name, Value from HTTP_Header into list of well formated "name: value" like in http header --- web/CXM_common.anubis | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/web/CXM_common.anubis b/web/CXM_common.anubis index aa627bb..71e2a60 100644 --- a/web/CXM_common.anubis +++ b/web/CXM_common.anubis @@ -12,7 +12,8 @@ *Name* HTTP_header *Description* -read system/string.anubis +transmit tools/basis.anubis +transmit system/string.anubis /** * The type 'HTTP_header' describes HTTP headers, which are just pairs '(name,value)'. @@ -39,6 +40,21 @@ public define Maybe(String) } }. +public define List(String) + to_List_String + ( + List(HTTP_header) l + )= + map((HTTP_header h) |-> h.name +": "+h.value, l ). + +public define String + to_String + ( + List(HTTP_header) l + )= + join("\n\r",to_List_String(l)). + + *Name* Web_arg *Description* -- libgit2 0.21.4