From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 16 Apr 2003 15:41:30 +0000 (+0000)
Subject: bugfix: print a better exception than "Not_found" when "baseuri"
X-Git-Tag: before_refactoring~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=af9dee32ed84a302d3ac0ba3005f9ecc0da7f46e;p=helm.git

bugfix: print a better exception than "Not_found" when "baseuri"
parameter for "ls" method is empty or simply unparsable
---

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 501b9d839..0792d30b5 100644
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -71,16 +71,21 @@ let parse_output_format (req: Http_types.request) =
 let parse_ls_uri =
   let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/+$" in
+  let wrong_uri uri =
+    raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ uri))
+  in
   fun (req: Http_types.request) ->
     let baseuri = req#param "baseuri" in
-    let subs =
-      Pcre.extract ~rex:parse_ls_RE
-        (Pcre.replace ~rex:trailing_slash_RE  baseuri)
-    in
-    match (subs.(1), subs.(2)) with
-    | "cic", uri -> Cic uri
-    | "theory", uri -> Theory uri
-    | _ -> raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ baseuri))
+    try
+      let subs =
+        Pcre.extract ~rex:parse_ls_RE
+          (Pcre.replace ~rex:trailing_slash_RE  baseuri)
+      in
+      (match (subs.(1), subs.(2)) with
+      | "cic", uri -> Cic uri
+      | "theory", uri -> Theory uri
+      | _ -> wrong_uri baseuri)
+    with Not_found -> wrong_uri baseuri
 ;;
 
   (* global maps, shared by all threads *)