added experimental yxml_find_theorems web service (but no client yet)

--- a/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
@@ -30,7 +30,8 @@
 
 $(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
   html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
-  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
+  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
+  ROOT.ML
 	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
 
 

--- a/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
@@ -11,5 +11,6 @@
   use "scgi_server.ML";
   use "echo.ML";
   use "html_templates.ML";
-  use "find_theorems.ML")
+  use "find_theorems.ML";
+  use "yxml_find_theorems.ML")
 else ()

--- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
@@ -124,7 +124,7 @@
 
 WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
 SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
-MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
+MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
 
 case "$COMMAND" in
   start)

--- a/src/Tools/WWW_Find/scgi_server.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML	Mon May 30 17:07:48 2011 +0200
@@ -12,6 +12,7 @@
   val server : string -> int -> unit
   val server' : int -> string -> int -> unit (* keeps trying for port *)
   val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
+  val raw_post_handler : (string -> string) -> handler
 end;
 
 structure ScgiServer : SCGI_SERVER =
@@ -132,5 +133,9 @@
    | ScgiReq.Head => raise Fail "Cannot handle Head requests.")
   send;
 
+fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
+      send (h (Byte.bytesToString content))
+  | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
+
 end;
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/yxml_find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -0,0 +1,47 @@
+(*  Title:      src/Pure/Tools/yxml_find_theorems.ML
+    Author:     Sree Harsha Totakura, TUM
+                Lars Noschinski, TUM
+                Alexander Krauss, TUM
+
+Simple find theorems web service with yxml interface for programmatic
+invocation.
+*)
+
+signature YXML_FIND_THEOREMS =
+sig
+  val init: unit -> unit
+end
+
+
+structure YXML_Find_Theorems : YXML_FIND_THEOREMS =
+struct
+
+val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *)
+
+fun yxml_find_theorems theorem_list yxml_query =
+  let
+    val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory);
+  in
+    Find_Theorems.query_of_xml (YXML.parse yxml_query)
+    |> Find_Theorems.filter_theorems ctxt theorem_list
+    ||> rev o (filter (fn Find_Theorems.External x => true | _ => false))
+    |> Find_Theorems.xml_of_result |> YXML.string_of
+  end;
+
+fun visible_facts facts =
+  Facts.dest_static [] facts
+  |> filter_out (Facts.is_concealed facts o #1);
+
+fun init () = 
+  let
+    val all_facts =
+      maps Facts.selections
+        (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory)))
+      |> map (Find_Theorems.External o apsnd prop_of);
+  in
+    ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*),
+      ScgiServer.raw_post_handler (yxml_find_theorems all_facts))
+  end;
+
+end;
+