# HG changeset patch # User krauss # Date 1306768068 -7200 # Node ID 6fde0c323c1558ac1ba229f0b8a4d2166e37fb93 # Parent 8b566f0d226c19e3824411cc505c40fcc4de4107 added experimental yxml_find_theorems web service (but no client yet) diff -r 8b566f0d226c -r 6fde0c323c15 src/Tools/WWW_Find/IsaMakefile --- 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 diff -r 8b566f0d226c -r 6fde0c323c15 src/Tools/WWW_Find/ROOT.ML --- 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 () diff -r 8b566f0d226c -r 6fde0c323c15 src/Tools/WWW_Find/lib/Tools/wwwfind --- 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) diff -r 8b566f0d226c -r 6fde0c323c15 src/Tools/WWW_Find/scgi_server.ML --- 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; diff -r 8b566f0d226c -r 6fde0c323c15 src/Tools/WWW_Find/yxml_find_theorems.ML --- /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; +