urimanager removed

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

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index f3656081f8f2861b93639b78460d8f201738717e..6221e4901c53ec37937d6e6488d7f82bea231937 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -67,7 +67,7 @@ let first_line s =
 
 type guistuff = {
   mathviewer:MatitaTypes.mathViewer;
-  urichooser: UriManager.uri list -> UriManager.uri list;
+  urichooser: NReference.reference list -> NReference.reference list;
   ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
 }
 
@@ -429,8 +429,7 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    NCicLibrary.time_travel
-     ((new GrafiteTypes.status cur_grafite_status#baseuri)#set_lstatus cur_grafite_status#lstatus);
+    NCicLibrary.time_travel grafite_status;
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)