From c2957e84a0fa8fe60bbbe89f4923a50bd626444d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jul 2008 11:43:26 +0000 Subject: [PATCH] universes in CicBrowser --- helm/software/matita/matita.glade | 64 ++++++++++++++++++++++---- helm/software/matita/matitaMathView.ml | 25 ++++++++++ helm/software/matita/matitaTypes.ml | 2 + helm/software/matita/matitaTypes.mli | 4 +- 4 files changed, 85 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 373ebb433..2e68ce487 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -113,14 +113,6 @@ - - - True - _Metadata - True - - - True @@ -140,8 +132,10 @@ - + True + Universes + True @@ -794,6 +788,58 @@ tab + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + False + False + False + + + + + False + True + + + + + + True + Universes + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + 0 diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 7f1917cfe..d8c02af44 100644 --- 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 0c8952e89..18aaa2e65 100644 --- 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 67655c921..20d042596 100644 --- 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 -- 2.39.2