fixed history handling: now both "home" and link reached via href are

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 1cb23366a2102ed820990e6e4a9dc87999655a1c..f22b3a170b6546d922721b78d56a0ad50bbb51d1 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -309,6 +309,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   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
+  let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
+  let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
+  let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
   let gui = MatitaGui.instance () in
   let win = gui#newBrowserWin () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
@@ -348,7 +351,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     with exn ->
       fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
   in
-  let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
+  let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
     inherit scriptAccessor
     
@@ -381,7 +384,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore (win#browserUri#connect#activate (handle_error' (fun () ->
         self#loadInput win#browserUri#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
-        self#_load (`About `Current_proof))));
+        self#load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
         (handle_error' self#refresh));
       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
@@ -396,22 +399,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           GMain.quit ();
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
-        ~callback:(fun _ _ ->
-          let selection = self#_getWhelpResultTreeviewSelection () in
-          let is_cic s =
-            try
-              String.sub s 0 5 = "cic:/"
-            with Invalid_argument _ -> false
-          in
-          let txt = 
-            if is_cic selection then
-              selection
-            else
-              win#browserUri#text ^ selection 
-          in
-          self#loadInput txt));
+        ~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 uri))));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -419,21 +409,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     val mutable current_infos = None
     val mutable current_mathml = None
 
-(*     val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview *)
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
-    method private _getWhelpResultTreeviewSelection () =
+    method private _getSelectedUri () =
       match model#easy_selection () with
-          | [u] -> u
-          | _ -> assert false
+      | [sel] when is_uri sel -> sel        (* absolute URI selected *)
+      | [sel] -> win#browserUri#text ^ sel  (* relative URI selected *)
+      | _ -> assert false
 
     (** history RATIONALE 
      *
-     * all operations about history are done using _historyFoo
-     *
-     * only toplevel function like load loadInput can call
-     * _historyAdd
+     * All operations about history are done using _historyFoo.
+     * Only toplevel functions (ATM load and loadInput) call _historyAdd.
      *)
           
     method private _historyAdd item = 
@@ -460,8 +448,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _showList = win#mathOrListNotebook#goto_page 1
     method private _showMath = win#mathOrListNotebook#goto_page 0
     
-
-    
     method private back () =
       try
         self#_load (self#_historyPrev ())
@@ -533,6 +519,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");
       self#_loadList l
 
     method private setEntry entry =
@@ -580,9 +567,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     (**  this is what the browser does when you enter a string an hit enter *)
     method loadInput txt =
       let txt = strip_blanks txt in
-      let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
-      let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
-      let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
       let fix_uri txt =
         UriManager.string_of_uri
           (UriManager.strip_xpointer (UriManager.uri_of_string txt))