many strings that are supposed to be URIs are now UriManager.uri

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index cdbfc799a054f28e1743e1e941507e240949d22e..8915f7681270ad43bdb94a009047820ac657f10d 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -402,6 +402,7 @@ let instance = singleton gui
 let non p x = not (p x)
 
 let is_var_uri s =
+  let s = UriManager.string_of_uri s in
   try
     String.sub s (String.length s - 4) 4 = ".var"
   with Invalid_argument _ -> false
@@ -446,7 +447,7 @@ let interactive_uri_choice
           | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
-    List.iter model#easy_append uris;
+    List.iter model#easy_append (List.map UriManager.string_of_uri uris);
     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
     let return v =
       choices := v;
@@ -464,11 +465,11 @@ let interactive_uri_choice
       connect_button dialog#uriChoiceAutoButton (fun _ ->
         match model#easy_selection () with
         | [] -> ()
-        | uris -> return (Some uris));
+        | uris -> return (Some (List.map UriManager.uri_of_string uris)));
     connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()
-      | uris -> return (Some uris));
+      | uris -> return (Some (List.map UriManager.uri_of_string uris)));
     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
     dialog#uriChoiceDialog#show ();
     GtkThread.main ();