--- /dev/null
+REQUIRES = http helm-cic_textual_parser helm-cic_proof_checking \
+ helm-xml gdome2-xslt helm-cic_unification helm-mathql \
+ helm-mathql_interpreter
+OCAMLOPTIONS = -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel -thread
+OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
+OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
+
+LIBRARIES = ../gTopLevel/mQueryGenerator.cmo
+LIBRARIES_OPT = ../gTopLevel/mQueryGenerator.cmx
+
+all: searchEngine
+opt: searchEngine.opt
+
+searchEngine: $(LIBRARIES) searchEngine.ml
+ $(OCAMLC) -linkpkg -o $@ $^
+searchEngine.opt: $(LIBRARIES_OPT) searchEngine.ml
+ $(OCAMLOPT) -linkpkg -o $@ $^
+
+clean:
+ rm -f *.cm[aiox] *.o searchEngine{,.opt}
+
+.PHONY: all opt clean
--- /dev/null
+
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+let debug = true;;
+let debug_print s = if debug then prerr_endline s;;
+Http_common.debug := debug;;
+
+open Printf;;
+
+let daemon_name = "Search Engine";;
+let default_port = 48085;;
+let port_env_var = "SEARCH_ENGINE_PORT";;
+
+let port =
+ try
+ int_of_string (Sys.getenv port_env_var)
+ with
+ | Not_found -> default_port
+ | Failure "int_of_string" ->
+ prerr_endline "Warning: invalid port, reverting to default";
+ default_port
+in
+let pp_result result =
+ let result_string = MQueryUtil.text_of_result result "\n" in
+ (sprintf "<html><body><pre>%s</pre></body></html>" result_string)
+in
+let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>" in
+let callback req outchan =
+ try
+ (* TODO catch exceptions *)
+ (match req#path with
+ | "/execute" ->
+ let query_string = req#param "query" in
+ let lexbuf = Lexing.from_string query_string in
+ let query = MQueryTParser.query MQueryTLexer.query_token lexbuf in
+ let result = MQueryGenerator.execute_query query in
+ let result_string = MQueryUtil.text_of_result result "\n" in
+ Http_daemon.respond
+ ~body:
+ (sprintf
+ "<html><body><pre>%s</pre></body></html>"
+ result_string)
+ outchan
+ | "/locate" ->
+ let id = req#param "id" in
+ let result = MQueryGenerator.locate id in
+ Http_daemon.respond ~body:(pp_result result) outchan
+ | "/searchPattern" ->
+ let term_string = req#param "term" in
+ let precision = int_of_string (req#param "precision") in
+ let lexbuf = Lexing.from_string term_string in
+ let (dom, mkterm) =
+ CicTextualParser.main CicTextualLexer.token lexbuf
+ in
+ (match dom with
+ | [] -> (* no free variables *)
+ let term = mkterm (fun _ -> None) in
+ let result = MQueryGenerator.searchPattern [] [] term precision in
+ Http_daemon.respond ~body:(pp_result result) outchan
+ | _ ->
+ Http_daemon.respond
+ ~body:(pp_error
+ "identifiers resolution in the environment not yet implemented")
+ outchan)
+ | invalid_request ->
+ Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan)
+ with
+ | Http_request.Param_not_found attr_name ->
+ Http_daemon.respond_error
+ ~status:(`Client_error `Bad_request)
+ ~body:(sprintf "Parameter '%s' is missing" attr_name)
+ outchan
+in
+printf "%s started and listening on port %d\n" daemon_name port;
+printf "current directory is %s\n" (Sys.getcwd ());
+flush stdout;
+Http_daemon.start' ~port callback;
+printf "%s is terminating, bye!\n" daemon_name
+
projects / helm.git / commitdiff