]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/main.ml
support for terms with metas in check
[helm.git] / helm / http_getter / main.ml
index faf899b80c0e9b2bdee6fa566b852f506a804523..640584e63a9729e2d03941162c5633039ac2c7a5 100644 (file)
 open Printf
 
 open Http_getter_common
+open Http_getter_const
 open Http_getter_misc
 open Http_getter_types
-open Http_getter_debugger
 
   (* constants *)
 
-let configuration_file = "/projects/helm/etc/http_getter.conf.xml"
+let configuration_file = BuildTimeOpts.conffile
 
 let common_headers = [
   "Cache-Control", "no-cache";
@@ -45,14 +45,14 @@ let common_headers = [
 
   (* HTTP queries argument parsing *)
 
-  (* parse encoding ("format" parameter), default is Enc_normal *)
+  (* parse encoding ("format" parameter), default is `Normal *)
 let parse_enc (req: Http_types.request) =
   try
     (match req#param "format" with
-    | "normal" -> Enc_normal
-    | "gz" -> Enc_gzipped
+    | "normal" -> `Normal
+    | "gz" -> `Gzipped
     | s -> raise (Bad_request ("Invalid format: " ^ s)))
-  with Http_types.Param_not_found _ -> Enc_normal
+  with Http_types.Param_not_found _ -> `Normal
 
   (* parse "patch_dtd" parameter, default is true *)
 let parse_patch (req: Http_types.request) =
@@ -66,30 +66,10 @@ let parse_patch (req: Http_types.request) =
   (* parse output format ("format" parameter), no default value *)
 let parse_output_format meth (req: Http_types.request) =
   match req#param "format" with
-  | s when String.lowercase s = "txt" -> Fmt_text
-  | s when String.lowercase s = "xml" -> Fmt_xml
+  | s when String.lowercase s = "txt" -> `Text
+  | s when String.lowercase s = "xml" -> `Xml
   | s -> raise (Bad_request ("Invalid /" ^ meth ^ " format: " ^ s))
 
-  (* parse "baseuri" format for /ls method, no default value *)
-let parse_ls_uri =
-  let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
-  let trailing_slash_RE = Pcre.regexp "/+$" in
-  let wrong_uri uri =
-    raise (Bad_request ("Invalid /ls baseuri: " ^ uri))
-  in
-  fun (req: Http_types.request) ->
-    let baseuri = req#param "baseuri" in
-    try
-      let subs =
-        Pcre.extract ~rex:parse_ls_RE
-          (Pcre.replace ~rex:trailing_slash_RE  baseuri)
-      in
-      (match (subs.(1), subs.(2)) with
-      | "cic", uri -> Cic uri
-      | "theory", uri -> Theory uri
-      | _ -> wrong_uri baseuri)
-    with Not_found -> wrong_uri baseuri
-
   (* parse "position" argument, default is 0 *)
 let parse_position (req: Http_types.request) =
   try
@@ -110,24 +90,44 @@ let parse_rdf_class (req: Http_types.request) =
   | "backward" -> `Backward
   | c -> raise (Bad_request ("Invalid RDF class: " ^ c))
 
+let xml_escape = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
+
+let html_tag ?exn () =
+  let xml_decl = "<?xml version=\"1.0\"?>\n" in
+  match exn with
+  | Some (exn, arg) ->
+      let (exn, arg) = (xml_escape exn, xml_escape arg) in
+      sprintf
+        "%s<html xmlns=\"%s\"\nxmlns:helm=\"%s\"\nhelm:exception=\"%s\"\nhelm:exception_arg=\"%s\">\n"
+        xml_decl xhtml_ns helm_ns exn arg
+  | None ->
+      sprintf "%s<html xmlns=\"%s\"\nxmlns:helm=\"%s\">\n"
+        xml_decl xhtml_ns helm_ns
+
 let mk_return_fun pp_fun contype msg outchan =
   Http_daemon.respond
     ~body:(pp_fun msg) ~headers:["Content-Type", contype] outchan
-let pp_error s =
-  sprintf "<html><body>Http Getter error: %s</body></html>" s
-let pp_internal_error s =
-  sprintf "<html><body>Http Getter Internal error: %s</body></html>" s
-let pp_msg s = sprintf "<html><body>%s</body></html>" s
+let pp_msg s = sprintf "%s<body>%s</body></html>" (html_tag ()) s
 let null_pp s = s
-let return_html_error = mk_return_fun pp_error "text/html"
-let return_html_internal_error = mk_return_fun pp_internal_error "text/html"
-let return_html_msg = mk_return_fun pp_msg "text/html"
-let return_html_raw = mk_return_fun null_pp "text/html"
+let return_html_error exn =
+  let pp_error s =
+    sprintf "%s\n<body>Http Getter error: <span style=\"color:red\">%s</span></body></html>"
+      (html_tag ~exn ()) s
+  in
+  mk_return_fun pp_error "text/xml"
+let return_html_internal_error exn =
+  let pp_internal_error s =
+    sprintf "%s\n<body>Http Getter Internal error: <span style=\"color:red\">%s</span></body></html>"
+      (html_tag ~exn ()) s
+  in
+  mk_return_fun pp_internal_error "text/xml"
+let return_html_msg = mk_return_fun pp_msg "text/xml"
+let return_html_raw = mk_return_fun null_pp "text/xml"
 let return_xml_raw = mk_return_fun null_pp "text/xml"
-let return_400 body outchan = Http_daemon.respond_error ~code:400 ~body outchan
+let return_400 exn body = return_html_error exn body
 
 let return_all_foo_uris doctype uris outchan =
-  Http_daemon.send_basic_headers ~code:200 outchan;
+  Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
   Http_daemon.send_header "Content-Type" "text/xml" outchan;
   Http_daemon.send_headers common_headers outchan;
   Http_daemon.send_CRLF outchan;
@@ -151,24 +151,24 @@ let return_all_foo_uris doctype uris outchan =
 let return_all_xml_uris fmt outchan =
  let uris = Http_getter.getalluris () in
   match fmt with
-   | Fmt_text ->
+   | `Text ->
       let buf = Buffer.create 10240 in
        List.iter (bprintf buf "%s\n") uris ;
        let body = Buffer.contents buf in
        Http_daemon.respond
          ~headers:(("Content-Type", "text/plain") :: common_headers)
          ~body outchan
-   | Fmt_xml ->
+   | `Xml ->
       return_all_foo_uris "alluris" uris outchan
   
 let return_all_rdf_uris classs outchan =
   return_all_foo_uris "allrdfuris" (Http_getter.getallrdfuris classs) outchan
 
-let return_ls xmluri fmt outchan =
-  let ls_items = Http_getter.ls xmluri in
+let return_ls regexp fmt outchan =
+  let ls_items = Http_getter.ls regexp in
   let buf = Buffer.create 10240 in
   (match fmt with
-  | Fmt_text ->
+  | `Text ->
       List.iter
         (function
           | Ls_section dir -> bprintf buf "dir, %s\n" dir
@@ -179,7 +179,7 @@ let return_ls xmluri fmt outchan =
               (string_of_ls_flag obj.body)
               (string_of_ls_flag obj.proof_tree))
         ls_items
-  | Fmt_xml ->
+  | `Xml ->
       Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
       bprintf buf "<!DOCTYPE ls SYSTEM \"%s/getdtd?uri=ls.dtd\">\n"
         (Lazy.force Http_getter_env.my_own_url);
@@ -214,12 +214,14 @@ let return_resolve uri outchan =
     return_xml_raw
       (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve uri))
       outchan
-  with Unresolvable_URI uri ->
-    return_xml_raw "<unresolved />\n" outchan
+  with
+  | Unresolvable_URI _ -> return_xml_raw "<unresolvable />\n" outchan
+  | Key_not_found _ -> return_xml_raw "<not_found />\n" outchan
 
 let return_list_servers outchan =
   return_html_raw
-    (sprintf "<html><body><table>\n%s\n</table></body></html>"
+    (sprintf "%s<body><table>\n%s\n</table></body></html>"
+      (html_tag ())
       (String.concat "\n"
         (List.map
           (fun (pos, server) ->
@@ -227,17 +229,18 @@ let return_list_servers outchan =
           (Http_getter.list_servers ()))))
     outchan
 
-let log_failure msg = debug_print ("Request not fulfilled: " ^ msg)
+let log_failure msg = Http_getter_logger.log ("Request not fulfilled: " ^ msg)
 
   (** given an action (i.e. a function which expects a logger and do something
    * using it as a logger), perform it sending its output incrementally to the
    * given output channel. Response is sent embedded in an HTML document.
    * Channel is closed afterwards. *)
 let send_log_to ?prepend action outchan =
-  Http_daemon.send_basic_headers ~code:200 outchan;
-  Http_daemon.send_header "Content-Type" "text/html" outchan;
+  Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
+  Http_daemon.send_header "Content-Type" "text/xml" outchan;
   Http_daemon.send_CRLF outchan;
-  output_string outchan "<html><body>\n"; flush outchan;
+  output_string outchan (sprintf "%s<body>\n" (html_tag ()));
+  flush outchan;
   (match prepend with
   | None -> ()
   | Some text -> output_string outchan text; flush outchan);
@@ -253,8 +256,8 @@ let send_log_to ?prepend action outchan =
 
 let callback (req: Http_types.request) outchan =
   try
-    debug_print ("Connection from " ^ req#clientAddr);
-    debug_print ("Received request: " ^ req#path);
+    Http_getter_logger.log ("Connection from " ^ req#clientAddr);
+    Http_getter_logger.log ("Received request: " ^ req#path);
     (match req#path with
     | "/help" -> return_help outchan
     | "/getxml" ->
@@ -268,12 +271,15 @@ let callback (req: Http_types.request) outchan =
     | "/getdtd" ->
         Http_getter_cache.respond_dtd ~patch:(parse_patch req)
           ~url:(sprintf "%s/%s"
-            (Helm_registry.get "getter.dtd_dir") (req#param "uri"))
+            (Lazy.force Http_getter_env.dtd_dir) (req#param "uri"))
           outchan
     | "/resolve" -> return_resolve (req#param "uri") outchan
     | "/register" ->
         Http_getter.register ~uri:(req#param "uri") ~url:(req#param "url");
         return_html_msg "Register done" outchan
+    | "/unregister" ->
+        Http_getter.unregister (req#param "uri");
+        return_html_msg "Unregister done" outchan
     | "/clean_cache" ->
         Http_getter.clean_cache ();
         return_html_msg "Done." outchan
@@ -303,23 +309,24 @@ let callback (req: Http_types.request) outchan =
        return_all_xml_uris (parse_output_format "getalluris" req) outchan
     | "/getallrdfuris" -> return_all_rdf_uris (parse_rdf_class req) outchan
     | "/ls" ->
-       return_ls (parse_ls_uri req) (parse_output_format "ls" req) outchan
+        return_ls (req#param "baseuri") (parse_output_format "ls" req) outchan
     | "/getempty" ->
         Http_daemon.respond ~body:Http_getter_const.empty_xml outchan
     | invalid_request ->
-        Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
-    debug_print "Done!\n"
+        Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
+          outchan);
+    Http_getter_logger.log "Done!\n"
   with
   | Http_types.Param_not_found attr_name ->
       let msg = sprintf "Parameter '%s' is missing" attr_name in
       log_failure msg;
-      return_400 msg outchan
+      return_400 ("bad_request", msg) msg outchan
   | Bad_request msg ->
       log_failure msg;
-      return_html_error msg outchan
+      return_html_error ("bad_request", msg) msg outchan
   | Internal_error msg ->
       log_failure msg;
-      return_html_internal_error msg outchan
+      return_html_internal_error ("internal_error", msg) msg outchan
   | Shell.Subprocess_error l ->
       let msgs =
         List.map
@@ -327,27 +334,40 @@ let callback (req: Http_types.request) outchan =
             sprintf "Command '%s' returned %s" cmd (string_of_proc_status code))
           l
       in
-      log_failure (String.concat ", " msgs);
-      return_html_internal_error (String.concat "<br />\n" msgs) outchan
-  | exc ->
-      let msg = "Uncaught exception: " ^ (Printexc.to_string exc) in
+      let msg = String.concat ", " msgs in
       log_failure msg;
-      return_html_error msg outchan
+      return_html_internal_error ("subprocess_error", msg)
+        (String.concat "<br />\n" msgs) outchan
+  | exc ->
+      let msg = "uncaught exception: " ^ (Printexc.to_string exc) in
+      (match exc with
+      | Http_getter_types.Key_not_found uri ->
+          return_html_error ("key_not_found", uri) msg outchan
+      | _ ->
+          log_failure msg;
+          return_html_error ("uncaught_exception", msg) msg outchan)
 
     (* Main *)
 
 let main () =
   Helm_registry.load_from configuration_file;
-  Http_getter_env.reload ();
+  Http_getter.init ();
   print_string (Http_getter_env.env_to_string ());
   flush stdout;
-  at_exit Http_getter.close_maps;
-  Sys.catch_break true;
-  try
-    Http_daemon.start' ~mode:`Thread
-      ~timeout:(Some 600) ~port:(Helm_registry.get_int "getter.port")
-      callback
-  with Sys.Break -> ()  (* 'close_maps' already registered with 'at_exit' *)
+  let batch_update =
+    try Sys.argv.(1) = "-update" with Invalid_argument _ -> false
+  in
+  if batch_update then  (* batch mode: performs update and exit *)
+    Http_getter.update ~logger:Http_getter.stdout_logger ()
+  else begin            (* daemon mode: start http daemon *)
+    at_exit Http_getter.close_maps;
+    Sys.catch_break true;
+    try
+      Http_daemon.start' ~mode:`Thread
+        ~timeout:(Some 600) ~port:(Lazy.force Http_getter_env.port)
+        callback
+    with Sys.Break -> ()  (* 'close_maps' already registered with 'at_exit' *)
+  end
 
 let _ = main ()