From: Stefano Zacchiroli Date: Fri, 3 Nov 2006 13:46:17 +0000 (+0000) Subject: preliminary support for hbugs X-Git-Tag: 0.4.95@7852~825 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=26bd030af58a7f4a5dff3c41ad5431e31e851d3e;p=helm.git preliminary support for hbugs added to the cicbrowser the CTRL-l binding for highlighting the URL (a-la-firefox) --- diff --git a/matita/matita.glade b/matita/matita.glade index 0f7b50cf8..b8ae58347 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -56,6 +56,15 @@ + + + True + Open _Location ... + True + + + + True @@ -129,6 +138,20 @@ True + + + + True + + + + + + True + HBugs Tutors + True + + @@ -615,6 +638,158 @@ tab + + + + True + False + 0 + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + False + False + False + + + + + 0 + True + True + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + True + gtk-refresh + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + True + gtk-remove + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + True + gtk-add + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + False + True + + + + + + True + HBugs + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + 0 diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 4b54f60ac..5ae8baab6 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -925,6 +925,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) match self#currentCicUri with | Some uri -> self#load (`Metadata (`Deps (`Back, uri))) | None -> ()); + connect_menu_item win#hBugsTutorsMenuItem (fun () -> + self#load (`HBugs `Tutors)); + connect_menu_item win#browserUrlMenuItem (fun () -> + win#browserUri#entry#misc#grab_focus ()); (* fill dep graph contextual menu *) let go_menu_item = @@ -1000,9 +1004,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * * Use only these functions to switch between the tabs *) - method private _showMath = win#mathOrListNotebook#goto_page 0 - method private _showList = win#mathOrListNotebook#goto_page 1 - method private _showGviz = win#mathOrListNotebook#goto_page 3 + method private _showMath = win#mathOrListNotebook#goto_page 0 + method private _showList = win#mathOrListNotebook#goto_page 1 + method private _showGviz = win#mathOrListNotebook#goto_page 3 + method private _showHBugs = win#mathOrListNotebook#goto_page 4 method private back () = try @@ -1030,6 +1035,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Development d -> self#_showDevelDeps d | `Dir dir -> self#_loadDir dir + | `HBugs `Tutors -> self#_loadHBugsTutors | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> self#dependencies dir uri () | `Uri uri -> self#_loadUriManagerUri uri @@ -1111,6 +1117,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) lastDir <- dir; self#_loadList l + method private _loadHBugsTutors = + self#_showHBugs + method private setEntry entry = win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry); current_entry <- entry @@ -1176,6 +1185,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) `Uri (UriManager.uri_of_string ((*fix_uri*) txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) | txt when is_metadata txt -> `Metadata (parse_metadata txt) + | "hbugs:/tutors/" -> `HBugs `Tutors | txt -> (try MatitaTypes.entry_of_string txt diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml index 239ec6c82..791713e56 100644 --- a/matita/matitaTypes.ml +++ b/matita/matitaTypes.ml @@ -40,10 +40,11 @@ type abouts = type mathViewer_entry = [ `About of abouts (* current proof *) - | `Check of string (* term *) + | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv | `Development of string - | `Dir of string (* "directory" in cic uris namespace *) + | `Dir of string (* "directory" in cic uris namespace *) + | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri (* cic object uri *) | `Whelp of string * UriManager.uri list (* query and results *) @@ -58,6 +59,7 @@ let string_of_entry = function | `Cic (_, _) -> "term:" | `Development d -> "devel:/" ^ d | `Dir uri -> uri + | `HBugs `Tutors -> "hbugs:/tutors/" | `Metadata meta -> "metadata:/" ^ (match meta with diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli index dd89ed79b..c2e3f40ed 100644 --- a/matita/matitaTypes.mli +++ b/matita/matitaTypes.mli @@ -33,6 +33,7 @@ type mathViewer_entry = | `Cic of Cic.term * Cic.metasenv | `Development of string | `Dir of string + | `HBugs of [ `Tutors ] | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri | `Whelp of string * UriManager.uri list ]