]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
utilities for creating environment dumps
[helm.git] / helm / searchEngine / searchEngine.ml
index d994ac11a361e336e8b51f0af720c7862197e1a0..f6e81e2d8aed36998c04503efe15ce7ca7f28052 100644 (file)
@@ -122,7 +122,7 @@ let query_kind_of_req (req: Http_types.request) =
   | "/hint" -> "Hint"
   | "/locate" -> "Locate"
   | "/elim" -> "Elim"
-  | _ -> assert false
+  | _ -> ""
 
   (* given a uri with a query part in input try to find in it a string
    * "&param_name=..." (where param_name is given). If found its value will be
@@ -135,6 +135,9 @@ let patch_param param_name param_value url =
   else
     sprintf "%s&%s=%s" url param_name param_value
 
+  (** HTML encoding, e.g.: "<" -> "&lt;" *)
+let html_encode = Netencoding.Html.encode_from_latin1
+
 let send_results results
   ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") 
    (req: Http_types.request) outchan
@@ -197,7 +200,7 @@ let send_results results
   let subst =
     (tag "SEARCH_ENGINE_URL", my_own_url) ::
     (tag "ADVANCED", advanced) ::
-    (tag "EXPRESSION", req#param "expression") ::
+    (tag "EXPRESSION", html_encode (req#param "expression")) ::
     add_param_substs req#params @
     (if advanced = "no" then
       [ tag "SIMPLE_CHECKED", "checked='true'";
@@ -293,7 +296,7 @@ let exec_action dbd (req: Http_types.request) outchan =
                        tag "ADVANCED", advanced;
                        tag "INTERPRETATIONS", html_interpretations;
                        tag "CURRENT_CHOICES", req#param "choices";
-                       tag "EXPRESSION", req#param "expression";
+                       tag "EXPRESSION", html_encode (req#param "expression");
                        tag "QUERY_KIND", query_kind;
                        tag "QUERY_SUMMARY", "disambiguation";
                        tag "ACTION", string_tail req#path ]
@@ -348,16 +351,16 @@ let callback dbd (req: Http_types.request) outchan =
     (match req#path with
     | "/getpage" ->
           (* TODO implement "is_permitted" *)
-        (let is_permitted _ = true in
+        (let is_permitted page = not (Pcre.pmatch ~pat:"/" page) in
         let page = req#param "url" in
+        let fname = sprintf "%s/%s" pages_dir page in
         let preprocess =
           (try
             bool_of_string (req#param "preprocess")
           with Invalid_argument _ | Http_types.Param_not_found _ -> false)
         in
         (match page with
-        | page when is_permitted page ->
-            (let fname = sprintf "%s/%s" pages_dir page in
+        | page when is_permitted page && Sys.file_exists fname ->
             Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
             Http_daemon.send_header "Content-Type" "text/html" outchan;
             Http_daemon.send_CRLF outchan;
@@ -374,7 +377,7 @@ let callback dbd (req: Http_types.request) outchan =
                     "\n"))
                 fname
             end else
-              Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan)
+              Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan
         | page -> Http_daemon.respond_forbidden ~url:page outchan))
     | "/help" -> Http_daemon.respond ~body:daemon_name outchan
     | "/locate" ->