annotate src/goodjava/webserver/Connection.java @ 1822:aeaf2b65c005

better parse tables
author Franklin Schmidt <fschmidt@gmail.com>
date Tue, 09 Jul 2024 12:46:27 -0600
parents 32e77b071e09
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1402
27efb1fcbcb5 move luan.lib to goodjava
Franklin Schmidt <fschmidt@gmail.com>
parents: 1347
diff changeset
1 package goodjava.webserver;
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
2
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
3 import java.io.InputStream;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
4 import java.io.OutputStream;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
5 import java.io.IOException;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
6 import java.net.Socket;
1402
27efb1fcbcb5 move luan.lib to goodjava
Franklin Schmidt <fschmidt@gmail.com>
parents: 1347
diff changeset
7 import goodjava.logging.Logger;
27efb1fcbcb5 move luan.lib to goodjava
Franklin Schmidt <fschmidt@gmail.com>
parents: 1347
diff changeset
8 import goodjava.logging.LoggerFactory;
27efb1fcbcb5 move luan.lib to goodjava
Franklin Schmidt <fschmidt@gmail.com>
parents: 1347
diff changeset
9 import goodjava.parser.ParseException;
1493
471ef3e6a84e more io
Franklin Schmidt <fschmidt@gmail.com>
parents: 1463
diff changeset
10 import goodjava.io.IoUtils;
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
11
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
12
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
13 final class Connection {
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
14 private static final Logger logger = LoggerFactory.getLogger(Connection.class);
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
15
1142
0f59eab45f3d webserver - threading
Franklin Schmidt <fschmidt@gmail.com>
parents: 1138
diff changeset
16 static void handle(Server server,Socket socket) {
0f59eab45f3d webserver - threading
Franklin Schmidt <fschmidt@gmail.com>
parents: 1138
diff changeset
17 new Connection(server,socket).handle();
0f59eab45f3d webserver - threading
Franklin Schmidt <fschmidt@gmail.com>
parents: 1138
diff changeset
18 }
0f59eab45f3d webserver - threading
Franklin Schmidt <fschmidt@gmail.com>
parents: 1138
diff changeset
19
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
20 private final Server server;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
21 private final Socket socket;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
22
1142
0f59eab45f3d webserver - threading
Franklin Schmidt <fschmidt@gmail.com>
parents: 1138
diff changeset
23 private Connection(Server server,Socket socket) {
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
24 this.server = server;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
25 this.socket = socket;
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
26 }
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
27
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
28 private void handle() {
1736
a02a75e3daa8 webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1607
diff changeset
29 String rawHead = "";
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
30 try {
1144
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
31 Request request = new Request();
1194
bd0420fb3dd0 handle ParseException in webserver
Franklin Schmidt <fschmidt@gmail.com>
parents: 1162
diff changeset
32 Response response;
1513
Franklin Schmidt <fschmidt@gmail.com>
parents: 1493
diff changeset
33 String contentType = null;
1194
bd0420fb3dd0 handle ParseException in webserver
Franklin Schmidt <fschmidt@gmail.com>
parents: 1162
diff changeset
34 try {
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
35 InputStream in = socket.getInputStream();
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
36 byte[] a = new byte[8192];
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
37 int endOfHeader;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
38 int size = 0;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
39 int left = a.length;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
40 outer: while(true) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
41 int n = in.read(a,size,left);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
42 if( n == -1 ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
43 if( size == 0 ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
44 socket.close();
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
45 return;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
46 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
47 throw new IOException("unexpected end of input at "+size);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
48 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
49 size += n;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
50 for( int i=0; i<=size-4; i++ ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
51 if( a[i]=='\r' && a[i+1]=='\n' && a[i+2]=='\r' && a[i+3]=='\n' ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
52 endOfHeader = i + 4;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
53 break outer;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
54 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
55 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
56 left -= n;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
57 if( left == 0 ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
58 byte[] a2 = new byte[2*a.length];
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
59 System.arraycopy(a,0,a2,0,size);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
60 a = a2;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
61 left = a.length - size;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
62 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
63 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
64 rawHead = new String(a,0,endOfHeader);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
65 //System.out.println(rawHead);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
66 request.rawHead = rawHead;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
67 RequestParser parser = new RequestParser(request);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
68 parser.parseHead();
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
69
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
70 String lenStr = (String)request.headers.get("content-length");
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
71 if( lenStr != null ) {
1801
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
72 int len;
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
73 try {
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
74 len = Integer.parseInt(lenStr);
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
75 } catch(NumberFormatException e) {
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
76 throw new WrappedRuntimeException(e);
32e77b071e09 webserver logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1770
diff changeset
77 }
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
78 byte[] body = new byte[len];
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
79 size -= endOfHeader;
1750
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
80 try {
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
81 System.arraycopy(a,endOfHeader,body,0,size);
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
82 } catch(ArrayIndexOutOfBoundsException e) {
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
83 throw new WrappedRuntimeException(e);
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
84 }
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
85 while( size < len ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
86 int n = in.read(body,size,len-size);
1144
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
87 if( n == -1 ) {
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
88 throw new IOException("unexpected end of input at "+size);
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
89 }
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
90 size += n;
ae0a048f3bc7 webserver - handle POST params
Franklin Schmidt <fschmidt@gmail.com>
parents: 1142
diff changeset
91 }
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
92 request.body = body;
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
93 //System.out.println(new String(request.body));
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
94 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
95
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
96 contentType = (String)request.headers.get("content-type");
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
97 if( contentType != null ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
98 contentType = contentType.toLowerCase();
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
99 if( contentType.equals("application/x-www-form-urlencoded") ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
100 parser.parseUrlencoded(null);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
101 } else if( contentType.equals("application/x-www-form-urlencoded; charset=utf-8") ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
102 parser.parseUrlencoded("utf-8");
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
103 } else if( contentType.startsWith("multipart/form-data;") ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
104 parser.parseMultipart();
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
105 } else if( contentType.equals("application/json") ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
106 parser.parseJson(null);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
107 } else if( contentType.equals("application/json; charset=utf-8") ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
108 parser.parseJson("utf-8");
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
109 } else {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
110 logger.info("unknown request content-type: "+contentType);
1194
bd0420fb3dd0 handle ParseException in webserver
Franklin Schmidt <fschmidt@gmail.com>
parents: 1162
diff changeset
111 }
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
112 }
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
113
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
114 String scheme = (String)request.headers.get("x-forwarded-proto");
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
115 if( scheme != null )
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
116 request.scheme = scheme;
1237
275d1b52dbce add Request.scheme
Franklin Schmidt <fschmidt@gmail.com>
parents: 1229
diff changeset
117
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
118 if( "text/event-stream".equals(request.headers.get("accept")) ) {
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
119 ServerSentEvents.add(socket,request);
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
120 return;
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
121 }
1738
9713f7fd50b3 server-sent events
Franklin Schmidt <fschmidt@gmail.com>
parents: 1736
diff changeset
122
1194
bd0420fb3dd0 handle ParseException in webserver
Franklin Schmidt <fschmidt@gmail.com>
parents: 1162
diff changeset
123 response = server.handler.handle(request);
bd0420fb3dd0 handle ParseException in webserver
Franklin Schmidt <fschmidt@gmail.com>
parents: 1162
diff changeset
124 } catch(ParseException e) {
1770
6c01d54edcac logging
Franklin Schmidt <fschmidt@gmail.com>
parents: 1752
diff changeset
125 logger.info("parse error\n"+rawHead.trim()+"\n",e);
1513
Franklin Schmidt <fschmidt@gmail.com>
parents: 1493
diff changeset
126 String msg = e.toString();
Franklin Schmidt <fschmidt@gmail.com>
parents: 1493
diff changeset
127 if( contentType != null )
Franklin Schmidt <fschmidt@gmail.com>
parents: 1493
diff changeset
128 msg = "invalid content for content-type " + contentType + "\n" + msg;
Franklin Schmidt <fschmidt@gmail.com>
parents: 1493
diff changeset
129 response = Response.errorResponse(Status.BAD_REQUEST,msg);
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
130 }
1607
fa066aaa068c nginx caching
Franklin Schmidt <fschmidt@gmail.com>
parents: 1513
diff changeset
131 response.headers.put("Connection","close");
fa066aaa068c nginx caching
Franklin Schmidt <fschmidt@gmail.com>
parents: 1513
diff changeset
132 response.headers.put("Content-Length",Long.toString(response.body.length));
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
133 byte[] header = response.toHeaderString().getBytes();
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
134
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
135 OutputStream out = socket.getOutputStream();
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
136 out.write(header);
1493
471ef3e6a84e more io
Franklin Schmidt <fschmidt@gmail.com>
parents: 1463
diff changeset
137 IoUtils.copyAll(response.body.content,out);
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
138 out.close();
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
139 socket.close();
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
140 } catch(IOException e) {
1736
a02a75e3daa8 webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1607
diff changeset
141 logger.info(rawHead.trim()+"\n",e);
1750
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
142 } catch(WrappedRuntimeException wrapped) {
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
143 RuntimeException e = (RuntimeException)wrapped.getCause();
1752
Franklin Schmidt <fschmidt@gmail.com>
parents: 1750
diff changeset
144 logger.warn(rawHead.trim()+"\n",e);
1750
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
145 throw e;
1736
a02a75e3daa8 webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1607
diff changeset
146 } catch(RuntimeException e) {
a02a75e3daa8 webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1607
diff changeset
147 logger.error(rawHead.trim()+"\n",e);
a02a75e3daa8 webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1607
diff changeset
148 throw e;
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
149 }
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
150 }
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
151
1750
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
152 private static final class WrappedRuntimeException extends Exception {
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
153 WrappedRuntimeException(RuntimeException e) {
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
154 super(e);
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
155 }
c7b3c327248a webserver error handling
Franklin Schmidt <fschmidt@gmail.com>
parents: 1738
diff changeset
156 }
1137
c123ee15f99b add webserver
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
157 }