X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fgetter.ml;h=e53d0a3b4a75cfbc0b5cec15da275cb4d30daca8;hb=970ba0021a992efe25ec374875dc127ff236cc74;hp=894bf3ea9ff0e45268d7928db536386ad54bfd8f;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/getter/getter.ml b/helm/ocaml/getter/getter.ml
index 894bf3ea9..e53d0a3b4 100644
--- a/helm/ocaml/getter/getter.ml
+++ b/helm/ocaml/getter/getter.ml
@@ -61,3 +61,35 @@ let register uri url =
     "?uri=" ^ (UriManager.string_of_uri uri) ^
     "&url=" ^ url)
 ;;
+
+exception Unresolved;;
+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
+ | Resolved of string
+
+let resolve uri =
+ (* deliver resolve request to http_getter *)
+ let doc =
+  ClientHTTP.get
+   (!getter_url ^ "resolve" ^ "?uri=" ^ (UriManager.string_of_uri uri))
+ in
+  let res = ref Unknown in
+   Pxp_yacc.process_entity Pxp_yacc.default_config (`Entry_content [])
+    (Pxp_yacc.create_entity_manager ~is_document:true Pxp_yacc.default_config
+     (Pxp_yacc.from_string doc))
+    (function
+        Pxp_yacc.E_start_tag ("url",["value",url],_) -> res := Resolved url
+      | Pxp_yacc.E_start_tag ("unresolved",[],_) -> res := Exception Unresolved
+      | Pxp_yacc.E_start_tag _ -> res := Exception UnexpectedGetterOutput
+      | _ -> ()
+    ) ;
+   match !res with
+      Unknown -> raise UnexpectedGetterOutput
+    | Exception e -> raise e
+    | Resolved url -> url
+;;