- commented out no longer needed macros Redo, Undo, Abort

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 5fe955b3ea5f8124e428b0a7fd28f1815472ee26..0a2e8f90df37fbb5b2423e782333086cf209ec68 100644 (file)
--- 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