]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/getter.ml
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / ocaml / getter / getter.ml
index 894bf3ea9ff0e45268d7928db536386ad54bfd8f..c1ba01016842009b23c6671ea9be62fa4f678784 100644 (file)
@@ -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 even-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
+;;