]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
many strings that are supposed to be URIs are now UriManager.uri
[helm.git] / helm / matita / matitaMathView.ml
index 9c8ef985b3657261512f356384ac8d67276befda..776a9ada579ce8748e8867ad98a1e22e27809ed5 100644 (file)
@@ -407,7 +407,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore(win#whelpResultTreeview#connect#row_activated 
         ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#load (`Uri uri))));
+        handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri)))));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -476,10 +476,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             | `Check term -> self#_loadCheck term
             | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
             | `Dir dir -> self#_loadDir dir
-            | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
+            | `Uri uri -> self#_loadUriManagerUri uri
             | `Whelp (query, results) -> 
                 set_whelp_query query;
-                self#_loadList (List.map (fun r -> "obj", r) results));
+                self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results));
             self#setEntry entry
           end
       with
@@ -583,7 +583,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       end else begin
         let entry =
           match txt with
-          | txt when is_uri txt -> `Uri (fix_uri txt)
+          | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
           | txt when is_dir txt -> `Dir (add_trailing_slash txt)
           | txt ->
               (try