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

correctly stored and remembered in history

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 2e2ef874e12af0bd0aa4fabd8ce8ce7f611b517e..4b82c9339a696b95e30244d2a97c28603804d2a8 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -517,105 +517,96 @@ Copyright (C) 2005,
          </child>
 
          <child>
-           <widget class="GtkFrame" id="frame1">
+           <widget class="GtkNotebook" id="mathOrListNotebook">
              <property name="visible">True</property>
-             <property name="label_xalign">0</property>
-             <property name="label_yalign">0</property>
-             <property name="shadow_type">GTK_SHADOW_NONE</property>
+             <property name="can_focus">True</property>
+             <property name="show_tabs">True</property>
+             <property name="show_border">True</property>
+             <property name="tab_pos">GTK_POS_TOP</property>
+             <property name="scrollable">False</property>
+             <property name="enable_popup">False</property>
 
              <child>
-               <widget class="GtkNotebook" id="mathOrListNotebook">
+               <widget class="GtkScrolledWindow" id="ScrolledBrowser">
                  <property name="visible">True</property>
                  <property name="can_focus">True</property>
-                 <property name="show_tabs">True</property>
-                 <property name="show_border">True</property>
-                 <property name="tab_pos">GTK_POS_TOP</property>
-                 <property name="scrollable">False</property>
-                 <property name="enable_popup">False</property>
+                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="shadow_type">GTK_SHADOW_NONE</property>
+                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
                  <child>
-                   <widget class="GtkScrolledWindow" id="ScrolledBrowser">
-                     <property name="visible">True</property>
-                     <property name="can_focus">True</property>
-                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                     <property name="shadow_type">GTK_SHADOW_NONE</property>
-                     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
-                     <child>
-                       <placeholder/>
-                     </child>
-                   </widget>
-                   <packing>
-                     <property name="tab_expand">False</property>
-                     <property name="tab_fill">True</property>
-                   </packing>
+                   <placeholder/>
                  </child>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
 
-                 <child>
-                   <widget class="GtkLabel" id="mathLabel">
-                     <property name="visible">True</property>
-                     <property name="label" translatable="yes">MathView</property>
-                     <property name="use_underline">False</property>
-                     <property name="use_markup">False</property>
-                     <property name="justify">GTK_JUSTIFY_LEFT</property>
-                     <property name="wrap">False</property>
-                     <property name="selectable">False</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xpad">0</property>
-                     <property name="ypad">0</property>
-                   </widget>
-                   <packing>
-                     <property name="type">tab</property>
-                   </packing>
-                 </child>
+             <child>
+               <widget class="GtkLabel" id="mathLabel">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">MathView</property>
+                 <property name="use_underline">False</property>
+                 <property name="use_markup">False</property>
+                 <property name="justify">GTK_JUSTIFY_LEFT</property>
+                 <property name="wrap">False</property>
+                 <property name="selectable">False</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xpad">0</property>
+                 <property name="ypad">0</property>
+               </widget>
+               <packing>
+                 <property name="type">tab</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkScrolledWindow" id="scrolledwindow9">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="shadow_type">GTK_SHADOW_IN</property>
+                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
                  <child>
-                   <widget class="GtkScrolledWindow" id="scrolledwindow9">
+                   <widget class="GtkTreeView" id="whelpResultTreeview">
                      <property name="visible">True</property>
                      <property name="can_focus">True</property>
-                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                     <property name="shadow_type">GTK_SHADOW_IN</property>
-                     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
-                     <child>
-                       <widget class="GtkTreeView" id="whelpResultTreeview">
-                         <property name="visible">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="headers_visible">False</property>
-                         <property name="rules_hint">False</property>
-                         <property name="reorderable">False</property>
-                         <property name="enable_search">True</property>
-                       </widget>
-                     </child>
+                     <property name="headers_visible">False</property>
+                     <property name="rules_hint">False</property>
+                     <property name="reorderable">False</property>
+                     <property name="enable_search">True</property>
                    </widget>
-                   <packing>
-                     <property name="tab_expand">False</property>
-                     <property name="tab_fill">True</property>
-                   </packing>
                  </child>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
 
-                 <child>
-                   <widget class="GtkLabel" id="listLabel">
-                     <property name="visible">True</property>
-                     <property name="label" translatable="yes">WhelpResults</property>
-                     <property name="use_underline">False</property>
-                     <property name="use_markup">False</property>
-                     <property name="justify">GTK_JUSTIFY_LEFT</property>
-                     <property name="wrap">False</property>
-                     <property name="selectable">False</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xpad">0</property>
-                     <property name="ypad">0</property>
-                   </widget>
-                   <packing>
-                     <property name="type">tab</property>
-                   </packing>
-                 </child>
+             <child>
+               <widget class="GtkLabel" id="listLabel">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">WhelpResults</property>
+                 <property name="use_underline">False</property>
+                 <property name="use_markup">False</property>
+                 <property name="justify">GTK_JUSTIFY_LEFT</property>
+                 <property name="wrap">False</property>
+                 <property name="selectable">False</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xpad">0</property>
+                 <property name="ypad">0</property>
                </widget>
+               <packing>
+                 <property name="type">tab</property>
+               </packing>
              </child>
            </widget>
            <packing>

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))