"include" command implemented.

[helm.git] / helm / ocaml / getter / http_getter.ml

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index e0a1a4658c500f3f74ed06820657138828cd3594..4094a7376268eb6a31036a874643e258cbad4e9a 100644 (file)
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -35,8 +35,6 @@ open Http_getter_types
 exception Not_implemented of string
 exception UnexpectedGetterOutput
 
-(* resolve_result is needed because it is not possible to raise *)
-(* an exception in a pxp ever-processing callback. Too bad.     *)
 type resolve_result =
   | Unknown
   | Exception of exn
@@ -44,17 +42,18 @@ type resolve_result =
 
 type logger_callback = HelmLogger.html_tag -> unit
 
-let stdout_logger tag =  print_string (HelmLogger.string_of_html_tag tag)
+let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag)
 
 let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
 
-let (index_line_sep_RE, index_sep_RE, trailing_types_RE,
-    heading_cic_RE, heading_theory_RE, heading_nuprl_RE,
-    heading_rdf_cic_RE, heading_rdf_theory_RE) =
-  (Pcre.regexp "[ \t]+", Pcre.regexp "\r\n|\r|\n",
-  Pcre.regexp "\\.types$",
-  Pcre.regexp "^cic:", Pcre.regexp "^theory:", Pcre.regexp "^nuprl:",
-  Pcre.regexp "^helm:rdf.*//cic:", Pcre.regexp "^helm:rdf.*//theory:")
+let index_line_sep_RE     = Pcre.regexp "[ \t]+"
+let index_sep_RE          = Pcre.regexp "\r\n|\r|\n"
+let trailing_types_RE     = Pcre.regexp "\\.types$"
+let heading_cic_RE        = Pcre.regexp "^cic:"
+let heading_theory_RE     = Pcre.regexp "^theory:"
+let heading_nuprl_RE     = Pcre.regexp "^nuprl:"
+let heading_rdf_cic_RE    = Pcre.regexp "^helm:rdf.*//cic:"
+let heading_rdf_theory_RE = Pcre.regexp "^helm:rdf.*//theory:"
 
   (* global maps, shared by all threads *)
 
@@ -260,33 +259,41 @@ let ls_remote lsuri = not_implemented "ls_remote"
 
 let resolve_remote uri =
   (* deliver resolve request to http_getter *)
-  let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in
+  let doc =
+    Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri)
+  in
   let res = ref Unknown in
-   Pxp_ev_parser.process_entity PxpHelmConf.pxp_config (`Entry_content [])
-    (Pxp_ev_parser.create_entity_manager ~is_document:true
-      PxpHelmConf.pxp_config (Pxp_yacc.from_string doc))
-    (function
-      | Pxp_types.E_start_tag ("url",["value",url],_,_) -> res := Resolved url
-      | Pxp_types.E_start_tag ("unresolvable",[],_,_) ->
-          res := Exception (Unresolvable_URI uri)
-      | Pxp_types.E_start_tag ("not_found",[],_,_) ->
-          res := Exception (Key_not_found uri)
-      | Pxp_types.E_start_tag (x,_,_,_) -> 
-         res := Exception UnexpectedGetterOutput
-      | _ -> ());
-   match !res with
-   | Unknown -> raise UnexpectedGetterOutput
-   | Exception e -> raise e
-   | Resolved url -> url
+  let start_element tag attrs =
+    match tag with
+    | "url" ->
+        (try
+          res := Resolved (List.assoc "value" attrs)
+        with Not_found -> ())
+    | "unresolvable" -> res := Exception (Unresolvable_URI uri)
+    | "not_found" -> res := Exception (Key_not_found uri)
+    | _ -> ()
+  in
+  let callbacks = {
+    XmlPushParser.default_callbacks with
+      XmlPushParser.start_element = Some start_element
+  } in
+  let xml_parser = XmlPushParser.create_parser callbacks in
+  XmlPushParser.parse xml_parser (`String doc);
+  XmlPushParser.final xml_parser;
+  match !res with
+  | Unknown -> raise UnexpectedGetterOutput
+  | Exception e -> raise e
+  | Resolved url -> url
 
 let register_remote ~uri ~url =
-  ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
+  Http_getter_wget.send
+    (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
 
 let unregister_remote uri =
-  ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri)
+  Http_getter_wget.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri)
 
 let update_remote logger  () =
-  let answer = ClientHTTP.get (getter_url () ^ "update") in
+  let answer = Http_getter_wget.get (getter_url () ^ "update") in
   logger (`T answer);
   logger `BR
 
@@ -297,7 +304,7 @@ let getxml_remote ~format ~patch_dtd uri =
       (match format with `Normal -> "normal" | `Gzipped -> "gz")
       (match patch_dtd with true -> "yes" | false -> "no")
   in
-  ClientHTTP.get_and_save_to_tmp uri
+  Http_getter_wget.get_and_save_to_tmp uri
 
 (* API *)
 
@@ -464,6 +471,7 @@ let basepart_RE =
     
 let (slash_RE, til_slash_RE, no_slashes_RE) =
   (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
+let fix_regexp_RE = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
   
 let ls regexp =
   if remote () then
@@ -475,6 +483,15 @@ let ls regexp =
       Pcre.regexp (pat ^ "/"), Pcre.regexp "[^/]+/[^/]*",
       Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp "/.*"
     in
+    let exists_theory regexp =
+      let theory =
+        Pcre.replace ~rex:fix_regexp_RE ~templ:"theory" regexp ^ "index.theory"
+      in
+      try
+        ignore (resolve theory);
+        true
+      with Key_not_found _ -> false
+    in
     let toplevel_theory =
       match List.rev (Pcre.split ~rex:slash_RE pat) with
       | dir :: _ -> Some (dir ^ ".theory")
@@ -606,7 +623,7 @@ let ls regexp =
             (index_not_generated_yet := false ;
              store_obj "index.theory"));
  *)
-    store_obj "index.theory";
+    if exists_theory regexp then store_obj "index.theory";
     List.iter
      (fun localpart ->
        if not (List.mem localpart !valid_candidates) then
@@ -638,13 +655,16 @@ let sync_dump_file () =
   
 let init () =
   Http_getter_logger.set_log_level
-    (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+    (Helm_registry.get_opt_default Helm_registry.int ~default:1
+      "getter.log_level");
   Http_getter_logger.set_log_file
-    (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+    (Helm_registry.get_opt Helm_registry.string "getter.log_file");
   Http_getter_env.reload ();
   let is_prefetch_set = 
-    Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch"
+    Helm_registry.get_opt_default Helm_registry.bool ~default:false
+      "getter.prefetch"
   in
   if is_prefetch_set then
-    ignore (Thread.create sync_with_map ())
+    (* ignore (Thread.create sync_with_map ()) *)
+    sync_with_map ()