]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
1. matitaEngine splitted into disambiguation (now in grafite_parser) and
[helm.git] / helm / matita / matitaMathView.ml
index 15a4a126d047384c86ef6f483f879f524fbe8dce..b637eb8dc37b9b7a06bb547ecb63fa5f8bae4445 100644 (file)
@@ -25,7 +25,7 @@
 
 open Printf
 
-open MatitaTypes
+open GrafiteTypes
 open MatitaGtkMisc
 
 module Stack = Continuationals.Stack
@@ -849,7 +849,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadList l
 
     method private setEntry entry =
-      win#browserUri#entry#set_text (string_of_entry entry);
+      win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =
@@ -892,10 +892,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
           | txt ->
-              (try
-                entry_of_string txt
+             (try
+               MatitaTypes.entry_of_string txt
               with Invalid_argument _ ->
-                command_error (sprintf "unsupported uri: %s" txt))
+               raise
+                (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
         in
         self#_load entry;
         self#_historyAdd entry