ported to new getter interface

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 2151541a32aa179f165b51993a97138dd16fa866..cd600f0403c4c663d18e9ad330124c8e1db63b78 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -300,8 +300,6 @@ type term_source =
   | `String of string
   ]
 
-exception Browser_failure of string
-
 class type cicBrowser =
 object
   method load: MatitaTypes.mathViewer_entry -> unit
@@ -309,6 +307,12 @@ object
   method loadInput: string -> unit
 end
 
+let reloadable = function
+  | `About `Current_proof
+  | `Dir _ ->
+      true
+  | _ -> false
+
 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   ()
 =
@@ -316,9 +320,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let whelp_RE = Pcre.regexp "^\\s*whelp" in
   let uri_RE =
     Pcre.regexp
-      "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
+      "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
   in
-  let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in
+  let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/$" in
   let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
@@ -361,8 +365,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let handle_error f =
     try
       f ()
-    with exn ->
-      fail (MatitaExcPp.to_string exn)
+    with exn -> fail (MatitaExcPp.to_string exn)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
@@ -404,9 +407,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           GMain.quit ();
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
-        ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
+        ~callback:(fun _ _ ->
+          handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri)))));
+        handle_error (fun () ->
+          self#load (`Uri (UriManager.uri_of_string uri)))));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -417,10 +422,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
+    val mutable lastDir = ""  (* last loaded "directory" *)
+
     method private _getSelectedUri () =
       match model#easy_selection () with
       | [sel] when is_uri sel -> sel  (* absolute URI selected *)
-      | [sel] -> win#browserUri#entry#text ^ sel  (* relative URI selected *)
+(*       | [sel] -> win#browserUri#entry#text ^ sel  |+ relative URI selected +| *)
+      | [sel] -> lastDir ^ sel
       | _ -> assert false
 
     (** history RATIONALE 
@@ -467,25 +475,22 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       * @param uri string *)
     method private _load entry =
       try
-          if entry <> current_entry || entry = `About `Current_proof then begin
-            (match entry with
-            | `About `Current_proof -> self#home ()
-            | `About `Blank -> self#blank ()
-            | `About `Us -> () (* TODO implement easter egg here :-] *)
-            | `Check term -> self#_loadCheck term
-            | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
-            | `Dir dir -> self#_loadDir dir
-            | `Uri uri -> self#_loadUriManagerUri uri
-            | `Whelp (query, results) -> 
-                set_whelp_query query;
-                self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results));
-            self#setEntry entry
-          end
-      with
-      | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri)
-      | CicEnvironment.Object_not_found uri ->
-          fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
-      | Browser_failure msg -> fail msg
+        if entry <> current_entry || reloadable entry then begin
+          (match entry with
+          | `About `Current_proof -> self#home ()
+          | `About `Blank -> self#blank ()
+          | `About `Us -> () (* TODO implement easter egg here :-] *)
+          | `Check term -> self#_loadCheck term
+          | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+          | `Dir dir -> self#_loadDir dir
+          | `Uri uri -> self#_loadUriManagerUri uri
+          | `Whelp (query, results) -> 
+              set_whelp_query query;
+              self#_loadList (List.map (fun r -> "obj",
+                UriManager.string_of_uri r) results));
+          self#setEntry entry
+        end
+      with exn -> fail (MatitaExcPp.to_string exn)
 
     method private blank () =
       self#_showMath;
@@ -524,7 +529,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
           content
       in
-      if l = [] then raise (Browser_failure "no such directory");
+      lastDir <- dir;
       self#_loadList l
 
     method private setEntry entry =
@@ -588,7 +593,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
               (try
                 entry_of_string txt
               with Invalid_argument _ ->
-                raise (Browser_failure (sprintf "unsupported uri: %s" txt)))
+                command_error (sprintf "unsupported uri: %s" txt))
         in
         self#_load entry;
         self#_historyAdd entry
@@ -604,10 +609,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method history = history
     method currentEntry = current_entry
     method refresh () =
-      if current_entry = `About `Current_proof then
-      self#_load (`About `Current_proof) 
-  end
+      if reloadable current_entry then self#_load current_entry
 
+  end
   
 let sequentsViewer ~(notebook:GPack.notebook)
   ~(sequentViewer:sequentViewer) ()