From fd372e069bbcaa96dc5b2eef04f341b28850d726 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 8 Jun 2005 20:17:03 +0000 Subject: [PATCH] - handles about:* uris in cicBrowser - added comboboxentry in cicBrowser (still ugly ...) --- helm/matita/.depend | 5 +- helm/matita/Makefile.in | 2 +- helm/matita/matita.glade | 468 +++++++++++++++------------------- helm/matita/matitaGui.ml | 21 +- helm/matita/matitaGui.mli | 8 +- helm/matita/matitaMathView.ml | 16 +- helm/matita/matitaTypes.ml | 7 + 7 files changed, 253 insertions(+), 274 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index 618c44629..95217b4b6 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -33,9 +33,9 @@ matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ - matitaEngine.cmi matitaScript.cmi + matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi matitaScript.cmi matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ - matitaEngine.cmx matitaScript.cmi + matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx matitaScript.cmi matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ matitaSync.cmi matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ @@ -46,6 +46,7 @@ matitaDisambiguator.cmi: matitaTypes.cmo matitaEngine.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi +matitaMathView.cmi: matitaTypes.cmo matitaMisc.cmi: matitaTypes.cmo matitaScript.cmi: matitaTypes.cmo matitaSync.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 155a36e08..bbf534b32 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -103,7 +103,7 @@ TAGS: cd ..; otags -vi -r ocaml/ matita/ #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli -.depend: +depend: $(OCAMLDEP) *.ml *.mli > .depend include .depend diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 4b82c9339..690e17749 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -110,332 +110,278 @@ Copyright (C) 2005, True 0 - 0.5 - GTK_SHADOW_OUT + 0 + GTK_SHADOW_NONE - + True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + False + 0 - + True - False - 0 + new browser win + True + True + GTK_RELIEF_NONE + False - + True - new browser win - True - True - GTK_RELIEF_NONE - False - - - - True - gtk-new - 4 - 0.5 - 0.5 - 0 - 0 - - + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 - - 0 - False - False - + + + 0 + False + False + + + + + + True + history back + True + True + GTK_RELIEF_NONE + True - + True - history back - True - True - GTK_RELIEF_NONE - True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 - + True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 + False + 2 - + True - False - 2 - - - - True - gtk-go-back - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + - - - True - - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + + + True + + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + 0 + False + False + - - 0 - False - False - + + + 0 + False + False + + - - - True - history forward - True - True - GTK_RELIEF_NONE - True - - - - True - gtk-go-forward - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - + + + True + history forward + True + True + GTK_RELIEF_NONE + True - + True - refresh - True - True - GTK_RELIEF_NONE - True - - - - True - gtk-refresh - 4 - 0.5 - 0.5 - 0 - 0 - - + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 - - 0 - False - False - + + + 0 + False + False + + - - - True - home - True - True - GTK_RELIEF_NONE - True - - - - True - gtk-home - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - + + + True + refresh + True + True + GTK_RELIEF_NONE + True - + True - gtk-jump-to + gtk-refresh 4 0.5 0.5 0 0 - - 3 - False - False - - - - - - True - cic uri - True - True - True - True - True - 0 - - True - * - False - - - 3 - True - True - + + + 0 + False + False + + - - - 20 - True - False - 0 - - - - - - - - - - - 0 - False - True - - + + + True + home + True + True + GTK_RELIEF_NONE + True - + True + gtk-home + 4 0.5 0.5 0 0 - - 0 - False - False - + + + 0 + False + False + + + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + 3 + False + False + + + + + + + + + + True + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NONE + True + False + False - + True - True - GTK_RELIEF_NONE - True - False - False + False + 0 - + True - False - 0 - - - - True - GTK_ARROW_DOWN - GTK_SHADOW_NONE - 0.5 - 0.5 - 0 - 0 - - - 0 - True - True - - + GTK_ARROW_DOWN + GTK_SHADOW_NONE + 0.5 + 0.5 + 0 + 0 + + 0 + True + True + - - 0 - False - False - + + 0 + False + False + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index d18b82d14..a17b9bfb1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -31,6 +31,14 @@ open MatitaMisc let gui_instance = ref None ;; +class type browserWin = + (* this class exists only because GEdit.combo_box_entry is not supported by + * lablgladecc :-(((( *) +object + inherit MatitaGeneratedGui.browserWin + method browserUri: GEdit.combo_box_entry +end + class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] @@ -275,9 +283,16 @@ class gui () = method main = main method newBrowserWin () = - let win = new browserWin () in - win#check_widgets (); - win + object (self) + inherit browserWin () + val combo = GEdit.combo_box_entry () + initializer + self#check_widgets (); + let combo_widget = combo#coerce in + browserHBox#add combo_widget; + browserHBox#reorder_child combo_widget ~pos:6 + method browserUri = combo + end method newUriDialog () = let dialog = new uriChoiceDialog () in diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index f517bbb9c..674f3702c 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -34,6 +34,12 @@ object method log_callback: MatitaLog.log_callback end +class type browserWin = +object + inherit MatitaGeneratedGui.browserWin + method browserUri: GEdit.combo_box_entry +end + (** @param fname name of the Glade file describing the GUI *) class type gui = object @@ -53,7 +59,7 @@ object * methods below create a new window on each invocation. You should * remember to destroy windows after use *) - method newBrowserWin: unit -> MatitaGeneratedGui.browserWin + method newBrowserWin: unit -> browserWin method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index f22b3a170..225738d58 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -381,8 +381,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; - ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#loadInput win#browserUri#text))); + ignore (win#browserUri#entry#connect#activate (handle_error' (fun () -> + self#loadInput win#browserUri#entry#text))); ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> self#load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked @@ -414,8 +414,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _getSelectedUri () = match model#easy_selection () with - | [sel] when is_uri sel -> sel (* absolute URI selected *) - | [sel] -> win#browserUri#text ^ sel (* relative URI selected *) + | [sel] when is_uri sel -> sel (* absolute URI selected *) + | [sel] -> win#browserUri#entry#text ^ sel (* relative URI selected *) | _ -> assert false (** history RATIONALE @@ -523,7 +523,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadList l method private setEntry entry = - win#browserUri#set_text (string_of_entry entry); + win#browserUri#entry#set_text (string_of_entry entry); current_entry <- entry method private _loadObj obj = @@ -579,7 +579,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) match txt with | txt when is_uri txt -> `Uri (fix_uri txt) | txt when is_dir txt -> `Dir (add_trailing_slash txt) - | _ -> raise (Browser_failure (sprintf "unsupported uri: %s" txt)) + | txt -> + (try + entry_of_string txt + with Invalid_argument _ -> + raise (Browser_failure (sprintf "unsupported uri: %s" txt))) in self#_load entry; self#_historyAdd entry diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 800ae1c7e..d7dc383b7 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -163,6 +163,13 @@ let string_of_entry = function | `Dir uri | `Uri uri -> uri | `Whelp (query, _) -> query +let entry_of_string = function + | "about:blank" -> `About `Blank + | "about:proof" -> `About `Current_proof + | "about:us" -> `About `Us + | _ -> (* only about entries supported ATM *) + raise (Invalid_argument "entry_of_string") + class type mathViewer = object (** @param reuse if set reused last opened cic browser otherwise -- 2.39.2