From d937fdd65dc2101eaf1e0d167bf5db249a6f9b6b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 8 Jun 2005 19:21:33 +0000 Subject: [PATCH] fixed history handling: now both "home" and link reached via href are correctly stored and remembered in history --- helm/matita/matita.glade | 155 ++++++++++++++++------------------ helm/matita/matitaMathView.ml | 44 +++------- 2 files changed, 87 insertions(+), 112 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 2e2ef874e..4b82c9339 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -517,105 +517,96 @@ Copyright (C) 2005, - + True - 0 - 0 - GTK_SHADOW_NONE + True + True + True + GTK_POS_TOP + False + False - + True True - True - True - GTK_POS_TOP - False - False + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - - - - False - True - + + + + False + True + + - - - True - MathView - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - + + + True + MathView + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT - + True True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - True - True - False - False - False - True - - + False + False + False + True - - False - True - + + + False + True + + - - - True - WhelpResults - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - + + + True + WhelpResults + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + tab + diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1cb23366a..f22b3a170 100644 --- 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)) -- 2.39.2