author | wenzelm |
Sat, 25 May 2013 17:40:44 +0200 | |
changeset 52147 | 9943f8067f11 |
parent 51085 | d90218288d51 |
child 53709 | 84522727f9d3 |
permissions | -rw-r--r-- |
33823 | 1 |
(* Title: Tools/WWW_Find/scgi_server.ML |
33817 | 2 |
Author: Timothy Bourke, NICTA |
3 |
||
4 |
Simple SCGI server. |
|
5 |
*) |
|
6 |
||
7 |
signature SCGI_SERVER = |
|
8 |
sig |
|
9 |
val max_threads : int Unsynchronized.ref |
|
10 |
type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit |
|
11 |
val register : (string * Mime.t option * handler) -> unit |
|
12 |
val server : string -> int -> unit |
|
13 |
val server' : int -> string -> int -> unit (* keeps trying for port *) |
|
43074 | 14 |
val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler |
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43074
diff
changeset
|
15 |
val raw_post_handler : (string -> string) -> handler |
33817 | 16 |
end; |
17 |
||
18 |
structure ScgiServer : SCGI_SERVER = |
|
19 |
struct |
|
20 |
val max_threads = Unsynchronized.ref 5; |
|
21 |
||
22 |
type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit; |
|
23 |
||
24 |
local |
|
25 |
val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table); |
|
26 |
in |
|
27 |
fun register (name, mime, f) = |
|
28 |
Unsynchronized.change servers (Symtab.update_new (name, (mime, f))); |
|
29 |
fun lookup name = Symtab.lookup (!servers) name; |
|
30 |
||
31 |
fun dump_handlers () = ( |
|
32 |
tracing(" with handlers:"); |
|
33 |
app (fn (x, _) => tracing (" - " ^ x)) (Symtab.dest (!servers))) |
|
34 |
end; |
|
35 |
||
36 |
fun server server_prefix port = |
|
37 |
let |
|
45066
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
45026
diff
changeset
|
38 |
val passive_sock = Socket_Util.init_server_socket (SOME "localhost") port; |
33817 | 39 |
|
40 |
val thread_wait = ConditionVar.conditionVar (); |
|
41 |
val thread_wait_mutex = Mutex.mutex (); |
|
42 |
||
43 |
local |
|
44 |
val threads = Unsynchronized.ref ([] : Thread.thread list); |
|
45 |
fun purge () = Unsynchronized.change threads (filter Thread.isActive); |
|
46 |
in |
|
47 |
fun add_thread th = Unsynchronized.change threads (cons th); |
|
48 |
||
49 |
fun launch_thread threadf = |
|
50 |
(purge (); |
|
51 |
if length (!threads) < (!max_threads) then () |
|
52 |
else (tracing ("Waiting for a free thread..."); |
|
53 |
ConditionVar.wait (thread_wait, thread_wait_mutex)); |
|
54 |
add_thread |
|
39155 | 55 |
(Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *) |
33817 | 56 |
(fn () => exception_trace threadf, |
57 |
[Thread.EnableBroadcastInterrupt true, |
|
58 |
Thread.InterruptState |
|
59 |
Thread.InterruptAsynchOnce]))) |
|
60 |
end; |
|
61 |
||
62 |
fun loop () = |
|
63 |
let |
|
64 |
val (sock, _)= Socket.accept passive_sock; |
|
65 |
||
45066
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
45026
diff
changeset
|
66 |
val (sin, sout) = Socket_Util.make_streams sock; |
33817 | 67 |
|
68 |
fun send msg = BinIO.output (sout, Byte.stringToBytes msg); |
|
69 |
fun send_log msg = (tracing msg; send msg); |
|
70 |
||
71 |
fun get_content (st, 0) = Word8Vector.fromList [] |
|
72 |
| get_content x = BinIO.inputN x; |
|
73 |
||
74 |
fun do_req () = |
|
75 |
let |
|
76 |
val (req as ScgiReq.Req {path_info, request_method, ...}, |
|
77 |
content_is) = |
|
78 |
ScgiReq.parse sin |
|
79 |
handle ScgiReq.InvalidReq s => |
|
80 |
(send |
|
81 |
(HttpUtil.reply_header (HttpStatus.bad_request, NONE, [])); |
|
82 |
raise Fail ("Invalid request: " ^ s)); |
|
83 |
val () = tracing ("request: " ^ path_info); |
|
84 |
in |
|
85 |
(case lookup (unprefix server_prefix path_info) of |
|
86 |
NONE => send (HttpUtil.reply_header (HttpStatus.not_found, NONE, [])) |
|
87 |
| SOME (NONE, f) => f (req, get_content content_is, send) |
|
88 |
| SOME (t, f) => |
|
89 |
(send (HttpUtil.reply_header (HttpStatus.ok, t, [])); |
|
90 |
if request_method = ScgiReq.Head then () |
|
91 |
else f (req, get_content content_is, send))) |
|
92 |
end; |
|
93 |
||
41522
42d13d00ccfb
more FIXMEs concerning bad catch-all exception handlers;
wenzelm
parents:
41491
diff
changeset
|
94 |
fun thread_req () = (* FIXME avoid handle e *) |
33817 | 95 |
(do_req () handle e => (warning (exnMessage e)); |
96 |
BinIO.closeOut sout handle e => warning (exnMessage e); |
|
97 |
BinIO.closeIn sin handle e => warning (exnMessage e); |
|
98 |
Socket.close sock handle e => warning (exnMessage e); |
|
99 |
tracing ("request done."); |
|
100 |
ConditionVar.signal thread_wait); |
|
101 |
in |
|
102 |
launch_thread thread_req; |
|
103 |
loop () |
|
104 |
end; |
|
105 |
in |
|
51085
d90218288d51
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
wenzelm
parents:
45066
diff
changeset
|
106 |
tracing ("SCGI server started on port " ^ string_of_int port ^ "."); |
33817 | 107 |
dump_handlers (); |
108 |
loop (); |
|
109 |
Socket.close passive_sock |
|
110 |
end; |
|
111 |
||
112 |
local |
|
113 |
val delay = 5; |
|
114 |
in |
|
115 |
fun server' 0 server_prefix port = (warning "Giving up."; exit 1) |
|
116 |
| server' countdown server_prefix port = |
|
117 |
server server_prefix port |
|
118 |
handle OS.SysErr ("bind failed", _) => |
|
119 |
(warning ("Could not acquire port " |
|
41491 | 120 |
^ string_of_int port ^ ". Trying again in " |
121 |
^ string_of_int delay ^ " seconds..."); |
|
33817 | 122 |
OS.Process.sleep (Time.fromSeconds delay); |
123 |
server' (countdown - 1) server_prefix port); |
|
124 |
end; |
|
125 |
||
43074 | 126 |
fun simple_handler h (ScgiReq.Req {request_method, query_string, ...}, content, send) = |
127 |
h (case request_method of |
|
128 |
ScgiReq.Get => query_string |
|
129 |
| ScgiReq.Post => |
|
130 |
content |
|
131 |
|> Byte.bytesToString |
|
132 |
|> HttpUtil.parse_query_string |
|
133 |
| ScgiReq.Head => raise Fail "Cannot handle Head requests.") |
|
134 |
send; |
|
135 |
||
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43074
diff
changeset
|
136 |
fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43074
diff
changeset
|
137 |
send (h (Byte.bytesToString content)) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43074
diff
changeset
|
138 |
| raw_post_handler _ _ = raise Fail "Can only handle POST request."; |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43074
diff
changeset
|
139 |
|
33817 | 140 |
end; |
141 |