X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.mli;h=c7a2c5c2ac865329caf9ef392d3d7d7ea6110bdb;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=8d1ae4b5c05e57e5a598661efce2ffe2a799b2fc;hpb=3af56c5a48f7cad33fd701e0061fe143e0e2a7c5;p=helm.git diff --git a/helm/ocaml/getter/http_getter.mli b/helm/ocaml/getter/http_getter.mli index 8d1ae4b5c..c7a2c5c2a 100644 --- a/helm/ocaml/getter/http_getter.mli +++ b/helm/ocaml/getter/http_getter.mli @@ -28,13 +28,26 @@ open Http_getter_types + (** {2 Loggers} *) + type logger_callback = HelmLogger.html_tag -> unit +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 + + (** does not fail if given uri does not exist *) +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 @@ -45,7 +58,9 @@ val add_server: ?logger:logger_callback -> ?position:int -> string -> unit val remove_server: ?logger:logger_callback -> int -> unit val getalluris: unit -> string list val getallrdfuris: [ `Forward | `Backward ] -> string list -val ls: xml_uri -> ls_item list + + (** @param regexp regular expression (PCRE syntax) over HELM URIs *) +val ls: string -> ls_item list (** {2 Shorthands} *) @@ -58,4 +73,5 @@ val register' : UriManager.uri -> string -> unit val close_maps: unit -> unit val update_from_one_server: ?logger:logger_callback -> string -> unit val has_server: int -> bool (* does a server with a given position exists? *) +val init: unit -> unit