X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaMathView.ml;h=0a2e8f90df37fbb5b2423e782333086cf209ec68;hb=e6708c10ad615233628900902101216cc2f5baf5;hp=5fe955b3ea5f8124e428b0a7fd28f1815472ee26;hpb=6b8da04f526b3484dc92f61a23a8e61e63422c13;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 5fe955b3e..0a2e8f90d 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -378,8 +378,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(win#whelpResultTreeview#connect#row_activated ~callback:(fun _ _ -> let selection = self#_getWhelpResultTreeviewSelection () in + let is_cic s = + try + String.sub s 0 5 = "cic:/" + with Invalid_argument _ -> false + in let txt = - if String.sub selection 0 5 = "cic:/" then + if is_cic selection then selection else win#browserUri#text ^ selection @@ -558,10 +563,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_uri txt = try let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in - ignore(Http_getter.resolve' u); true + ignore (Http_getter.resolve' u); + true with | Http_getter_types.Key_not_found _ - | Http_getter_types.Unresolvable_URI _ -> false + | Http_getter_types.Unresolvable_URI _ + | UriManager.IllFormedUri ("cic:/" | "cic:") -> false | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'") in let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in