From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 13:16:58 +0000 (+0000) Subject: - API change (renamed some exceptions) X-Git-Tag: V_0_0_10~58 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae1f66ceadc14c7d0824bb375c5af175b15f083c;p=helm.git - API change (renamed some exceptions) - ported to the latest PXP version --- 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 () diff --git a/helm/ocaml/getter/http_getter.mli b/helm/ocaml/getter/http_getter.mli index c6f08afcc..f0b32b384 100644 --- a/helm/ocaml/getter/http_getter.mli +++ b/helm/ocaml/getter/http_getter.mli @@ -37,8 +37,17 @@ val stdout_logger: logger_callback (** {2 Getter Web Service interface as API *) val help: unit -> string + + (** @raise Http_getter_types.Unresolvable_URI _ + * @raise Http_getter_types.Key_not_found _ *) val resolve: string -> string (* uri -> url *) + + (** @raise Http_getter_types.Key_already_in _ *) val register: uri:string -> url:string -> unit + + (** @raise Http_getter_types.Key_not_found _ *) +val unregister: string -> unit + val update: ?logger:logger_callback -> unit -> unit val getxml : ?format:encoding -> ?patch_dtd:bool -> string -> string val getxslt : ?patch_dtd:bool -> string -> string diff --git a/helm/ocaml/getter/http_getter_map.ml b/helm/ocaml/getter/http_getter_map.ml index 2b61e7976..4bead0c6c 100644 --- a/helm/ocaml/getter/http_getter_map.ml +++ b/helm/ocaml/getter/http_getter_map.ml @@ -26,8 +26,7 @@ * http://helm.cs.unibo.it/ *) -exception Key_already_in of string;; -exception Key_not_found of string;; +open Http_getter_types class map dbname = let perm = 420 in (* permission 644 in decimal notation *) diff --git a/helm/ocaml/getter/http_getter_map.mli b/helm/ocaml/getter/http_getter_map.mli index 7081f1962..3e4ac7ba4 100644 --- a/helm/ocaml/getter/http_getter_map.mli +++ b/helm/ocaml/getter/http_getter_map.mli @@ -26,9 +26,6 @@ * http://helm.cs.unibo.it/ *) -exception Key_already_in of string -exception Key_not_found of string - class map: string -> object diff --git a/helm/ocaml/getter/http_getter_types.ml b/helm/ocaml/getter/http_getter_types.ml index 172cf18a9..e8e31bd0f 100644 --- a/helm/ocaml/getter/http_getter_types.ml +++ b/helm/ocaml/getter/http_getter_types.ml @@ -34,6 +34,8 @@ exception Invalid_RDF_class of string exception Internal_error of string exception Cache_failure of string exception Dtd_not_found of string (* dtd's url *) +exception Key_already_in of string;; +exception Key_not_found of string;; type encoding = [ `Normal | `Gzipped ] type answer_format = [ `Text | `Xml ]