X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=35a19db82bb4f5fc06afe990421085d09e147e81;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=a9884596ba62fe71ab7acfaf8f6981a49bf73c0e;hpb=11469c708704f96fde66e5bbc297f51a58173fb1;p=helm.git diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index a9884596b..35a19db82 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -222,12 +222,14 @@ let resolve_remote uri = 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)) + (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 ("unresolved",[],_,_) -> + | 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 _ -> res := Exception UnexpectedGetterOutput | _ -> ()); match !res with @@ -238,8 +240,8 @@ let resolve_remote uri = let register_remote ~uri ~url = ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) -let register_remote ~uri ~url = - ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) +let unregister_remote uri = + ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) let update_remote logger () = let answer = ClientHTTP.get (getter_url () ^ "update") in @@ -261,17 +263,20 @@ let resolve uri = if remote () then resolve_remote uri else - try - (map_of_uri uri)#resolve uri - with Http_getter_map.Key_not_found _ -> raise (Unresolvable_URI uri) + (map_of_uri uri)#resolve uri - (* Warning: this fail if uri is already registered *) let register ~uri ~url = if remote () then register_remote ~uri ~url else (map_of_uri uri)#add uri url +let unregister uri = + if remote () then + unregister_remote uri + else + (map_of_uri uri)#remove uri + let update ?(logger = fun _ -> ()) () = if remote () then update_remote logger ()