src/Tools/WWW_Find/find_theorems.ML
changeset 43074 8b566f0d226c
parent 43073 a4c985fe015d
child 51949 f6858bb224c9
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -11,17 +11,7 @@
 
 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
 
-fun parse_request (ScgiReq.Req {request_method, query_string, ...}, content, send) =
-  (case request_method of
-     ScgiReq.Get => query_string
-   | ScgiReq.Post =>
-      content
-      |> Byte.bytesToString
-      |> HttpUtil.parse_query_string
-   | ScgiReq.Head => raise Fail "Cannot handle Head requests.",
-  send);
-
-fun find_theorems (arg_data, send) =
+fun find_theorems arg_data send =
   let
     val args = Symtab.lookup arg_data;
 
@@ -66,7 +56,7 @@
 in
 
 val () = Printer.show_question_marks_default := false;
-val () = ScgiServer.register ("find_theorems", SOME Mime.html, find_theorems o parse_request);
+val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
 
 end;