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 0f7b50cf891b1626de57802acd9104b27a118710..b8ae5834748e1a360cf104a246145a105300d77b 100644 (file)
--- a/matita/matita.glade
+++ b/matita/matita.glade
@@ -56,6 +56,15 @@
                        </widget>
                      </child>
 
+                     <child>
+                       <widget class="GtkMenuItem" id="BrowserUrlMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label" translatable="yes">Open _Location ...</property>
+                         <property name="use_underline">True</property>
+                         <accelerator key="L" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+                       </widget>
+                     </child>
+
                      <child>
                        <widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
                          <property name="visible">True</property>
@@ -129,6 +138,20 @@
                          <property name="use_underline">True</property>
                        </widget>
                      </child>
+
+                     <child>
+                       <widget class="GtkSeparatorMenuItem" id="separator11">
+                         <property name="visible">True</property>
+                       </widget>
+                     </child>
+
+                     <child>
+                       <widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label" translatable="yes">HBugs Tutors</property>
+                         <property name="use_underline">True</property>
+                       </widget>
+                     </child>
                    </widget>
                  </child>
                </widget>
@@ -615,6 +638,158 @@
                  <property name="type">tab</property>
                </packing>
              </child>
+
+             <child>
+               <widget class="GtkVBox" id="vbox16">
+                 <property name="visible">True</property>
+                 <property name="homogeneous">False</property>
+                 <property name="spacing">0</property>
+
+                 <child>
+                   <widget class="GtkScrolledWindow" id="scrolledwindow13">
+                     <property name="visible">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+                     <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+                     <property name="shadow_type">GTK_SHADOW_NONE</property>
+                     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                     <child>
+                       <widget class="GtkTreeView" id="HBugsTutorsList">
+                         <property name="visible">True</property>
+                         <property name="can_focus">True</property>
+                         <property name="headers_visible">True</property>
+                         <property name="rules_hint">False</property>
+                         <property name="reorderable">False</property>
+                         <property name="enable_search">True</property>
+                         <property name="fixed_height_mode">False</property>
+                         <property name="hover_selection">False</property>
+                         <property name="hover_expand">False</property>
+                       </widget>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">True</property>
+                     <property name="fill">True</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkToolbar" id="toolbar3">
+                     <property name="visible">True</property>
+                     <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+                     <property name="tooltips">True</property>
+                     <property name="show_arrow">True</property>
+
+                     <child>
+                       <widget class="GtkToolItem" id="toolitem47">
+                         <property name="visible">True</property>
+                         <property name="visible_horizontal">True</property>
+                         <property name="visible_vertical">True</property>
+                         <property name="is_important">False</property>
+
+                         <child>
+                           <widget class="GtkButton" id="HBugsRefreshButton">
+                             <property name="visible">True</property>
+                             <property name="can_focus">True</property>
+                             <property name="label">gtk-refresh</property>
+                             <property name="use_stock">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
+                           </widget>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="expand">False</property>
+                         <property name="homogeneous">False</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkToolItem" id="toolitem48">
+                         <property name="visible">True</property>
+                         <property name="visible_horizontal">True</property>
+                         <property name="visible_vertical">True</property>
+                         <property name="is_important">False</property>
+
+                         <child>
+                           <widget class="GtkButton" id="HBugsUnsubscribeButton">
+                             <property name="visible">True</property>
+                             <property name="can_focus">True</property>
+                             <property name="label">gtk-remove</property>
+                             <property name="use_stock">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
+                           </widget>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="expand">False</property>
+                         <property name="homogeneous">False</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkToolItem" id="toolitem49">
+                         <property name="visible">True</property>
+                         <property name="visible_horizontal">True</property>
+                         <property name="visible_vertical">True</property>
+                         <property name="is_important">False</property>
+
+                         <child>
+                           <widget class="GtkButton" id="HBugsSubscribeButton">
+                             <property name="visible">True</property>
+                             <property name="can_focus">True</property>
+                             <property name="label">gtk-add</property>
+                             <property name="use_stock">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
+                           </widget>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="expand">False</property>
+                         <property name="homogeneous">False</property>
+                       </packing>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkLabel" id="label29">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">HBugs</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>
+                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                 <property name="width_chars">-1</property>
+                 <property name="single_line_mode">False</property>
+                 <property name="angle">0</property>
+               </widget>
+               <packing>
+                 <property name="type">tab</property>
+               </packing>
+             </child>
            </widget>
            <packing>
              <property name="padding">0</property>

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 4b54f60ac1e7f36bdd355147166e9790f53476fa..5ae8baab6ea2f6ee0943bdf723d275be0d3e8c4c 100644 (file)
--- 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 239ec6c823af485c91925fdf1d3aca5694e7ef4d..791713e56a4b5e13f2fa302cf7c87dac52796c6d 100644 (file)
--- 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 dd89ed79b82ed1783038e8af830c012e67ad51fc..c2e3f40ed3a87e0633d4ec16d777371972255133 100644 (file)
--- 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 ]