]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/http_getter.ml
uses XmlPushParser instead of Pxp for parsing getter resolve answer
[helm.git] / helm / ocaml / getter / http_getter.ml
index d0ecf9ba22d241851933a343fd6406a82cc390cb..58c94ac957c8dc2ccce93d7546f7bed42ea53ff8 100644 (file)
@@ -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
@@ -262,22 +260,26 @@ let resolve_remote uri =
   (* deliver resolve request to http_getter *)
   let doc = ClientHTTP.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);
+  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)