universes in CicBrowser

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 373ebb433d973f53f81cd3381ca51a132282b87d..2e68ce4871822451a1f4131ee082cab8900990eb 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -113,14 +113,6 @@
                  <child>
                    <widget class="GtkMenu" id="BrowserViewMenu_menu">
 
-                     <child>
-                       <widget class="GtkMenuItem" id="BrowserMetadataMenuItem">
-                         <property name="visible">True</property>
-                         <property name="label" translatable="yes">_Metadata</property>
-                         <property name="use_underline">True</property>
-                       </widget>
-                     </child>
-
                      <child>
                        <widget class="GtkMenuItem" id="DepGraphMenuItem">
                          <property name="visible">True</property>
@@ -140,8 +132,10 @@
                      </child>
 
                      <child>
-                       <widget class="GtkSeparatorMenuItem" id="separator11">
+                       <widget class="GtkMenuItem" id="univMenuItem">
                          <property name="visible">True</property>
+                         <property name="label" translatable="yes">Universes</property>
+                         <property name="use_underline">True</property>
                        </widget>
                      </child>
 
@@ -794,6 +788,58 @@
                  <property name="type">tab</property>
                </packing>
              </child>
+
+             <child>
+               <widget class="GtkScrolledWindow" id="scrolledwindow15">
+                 <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>
+                   <widget class="GtkTreeView" id="universesTreeview">
+                     <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="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkLabel" id="universes">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">Universes</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/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 7f1917cfe1cf5ce6c3642966aaebd54ad1846546..d8c02af44df108cbc2afc2cc1cdf7a23177f85cf 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -934,6 +934,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#hBugsTutorsMenuItem#misc#hide ();
       connect_menu_item win#browserUrlMenuItem (fun () ->
         win#browserUri#entry#misc#grab_focus ());
+      connect_menu_item win#univMenuItem (fun () ->
+        match self#currentCicUri with
+        | Some uri -> self#load (`Univs uri)
+        | None -> ());
 
       (* fill dep graph contextual menu *)
       let go_menu_item =
@@ -970,6 +974,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
+    val model_univs =
+      new MatitaGtkMisc.multiStringListModel ~cols:2 win#universesTreeview
 
     val mutable lastDir = ""  (* last loaded "directory" *)
 
@@ -1011,6 +1017,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
      *)
     method private _showMath = win#mathOrListNotebook#goto_page  0
     method private _showList = win#mathOrListNotebook#goto_page  1
+    method private _showList2 = win#mathOrListNotebook#goto_page 5
     method private _showGviz = win#mathOrListNotebook#goto_page  3
     method private _showHBugs = win#mathOrListNotebook#goto_page 4
 
@@ -1044,6 +1051,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
               self#dependencies dir uri ()
           | `Uri uri -> self#_loadUriManagerUri uri
+          | `Univs uri -> self#_loadUnivs uri
           | `Whelp (query, results) -> 
               set_whelp_query query;
               self#_loadList (List.map (fun r -> "obj",
@@ -1107,6 +1115,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let uri = UriManager.strip_xpointer uri in
       let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
       self#_loadObj obj
+
+    method private _loadUnivs uri =
+      let uri = UriManager.strip_xpointer uri in
+      let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+      let _,us = CicUniv.do_rank u in
+      let l = 
+        List.map 
+          (fun u -> 
+           [ CicUniv.string_of_universe u ; string_of_int (CicUniv.get_rank u)])
+          us 
+      in
+      self#_loadList2 l
       
     method private _loadDir dir = 
       let content = Http_getter.ls ~local:false dir in
@@ -1147,6 +1167,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       model#list_store#clear ();
       List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
       self#_showList
+
+    method private _loadList2 l =
+      model_univs#list_store#clear ();
+      List.iter model_univs#easy_mappend l;
+      self#_showList2
     
     (** { public methods, all must call _load!! } *)
       

diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml
index 0c8952e89777016f954536df2f416895c5d0a6fc..18aaa2e6552a58c7cf4247d750cb143a6013505d 100644 (file)
--- a/helm/software/matita/matitaTypes.ml
+++ b/helm/software/matita/matitaTypes.ml
@@ -48,6 +48,7 @@ type mathViewer_entry =
   | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
   | `Uri of UriManager.uri (* cic object uri *)
   | `Whelp of string * UriManager.uri list (* query and results *)
+  | `Univs of UriManager.uri
   ]
 
 let string_of_entry = function
@@ -72,6 +73,7 @@ let string_of_entry = function
           (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri)
   | `Uri uri -> UriManager.string_of_uri uri
   | `Whelp (query, _) -> query
+  | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri
 
 let entry_of_string = function
   | "about:blank" -> `About `Blank

diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli
index 67655c921e449e68106976f7bbda2dea8b556e0f..20d04259678f84937d097f731ea07c75bea9d238 100644 (file)
--- a/helm/software/matita/matitaTypes.mli
+++ b/helm/software/matita/matitaTypes.mli
@@ -35,7 +35,9 @@ type mathViewer_entry =
   | `HBugs of [ `Tutors ]
   | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
   | `Uri of UriManager.uri
-  | `Whelp of string * UriManager.uri list ]
+  | `Whelp of string * UriManager.uri list 
+  | `Univs of UriManager.uri
+  ]
 
 val string_of_entry : mathViewer_entry -> string
 val entry_of_string : string -> mathViewer_entry