- handles about:* uris in cicBrowser

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 800ae1c7e2c569bc1cb604c7ae5a32d5df16b9fd..d7dc383b7757fc5d4da9c6a5b9d34abe99bb95f1 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -163,6 +163,13 @@ let string_of_entry = function
   | `Dir uri | `Uri uri -> uri
   | `Whelp (query, _) -> query
 
+let entry_of_string = function
+  | "about:blank" -> `About `Blank
+  | "about:proof" -> `About `Current_proof
+  | "about:us"    -> `About `Us
+  | _ ->  (* only about entries supported ATM *)
+      raise (Invalid_argument "entry_of_string")
+
 class type mathViewer =
   object
     (** @param reuse if set reused last opened cic browser otherwise