package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/src/lambdapi.tool/websearch.ml.html
Source file websearch.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55#1 "src/tool/websearch.eml.ml" let show_form ?(message="") ?output request = let ___eml_buffer = Buffer.create 4096 in (Buffer.add_string ___eml_buffer "<html>\n<body>\n\n <h1><a href=\"https://github.com/Deducteam/lambdapi\">LambdaPi</a>\n Search Engine</h1>\n\n <p>\n The <b>search</b> button answers the query. Read the <a\n href=\"https://lambdapi.readthedocs.io/en/latest/query_language.html\">query\n language specification</a> to learn about the query language.<br>\n </p>\n\n <form method=\"POST\" action=\"/\">\n "); (Printf.bprintf ___eml_buffer "%s" ( #15 "src/tool/websearch.eml.ml" Dream.csrf_tag request )); (Buffer.add_string ___eml_buffer "\n <p>\n <input type=\"search\" required=\"true\" size=\"100\"\n name=\"message\" value=\""); (Printf.bprintf ___eml_buffer "%s" (Dream.html_escape ( #18 "src/tool/websearch.eml.ml" message ))); (Buffer.add_string ___eml_buffer "\"\n onfocus=\"this.select();\" autofocus></p>\n <p>\n <input type=\"submit\" value=\"search\" name=\"search\">\n </p>\n </form>\n\n"); #25 "src/tool/websearch.eml.ml" begin match output with #26 "src/tool/websearch.eml.ml" | None -> () #27 "src/tool/websearch.eml.ml" | Some output -> (Buffer.add_string ___eml_buffer " "); (Printf.bprintf ___eml_buffer "%s" ( #28 "src/tool/websearch.eml.ml" output )); (Buffer.add_string ___eml_buffer "\n"); #29 "src/tool/websearch.eml.ml" end; (Buffer.add_string ___eml_buffer "\n</body>\n</html>\n\n"); (Buffer.contents ___eml_buffer) #34 "src/tool/websearch.eml.ml" let start ~port () = Dream.run ~port @@ Dream.logger @@ Dream.memory_sessions @@ Dream.router [ Dream.get "/" (fun request -> Dream.html (show_form request)); Dream.post "/" (fun request -> match%lwt Dream.form request with | `Ok [ "message", message; "search", _search ] -> let output = Indexing.search_cmd_html message in Dream.html (show_form ~message ~output request) | _ -> Dream.empty `Bad_Request); ]