--- /dev/null
+Andrea Asperti <asperti@cs.unibo.it>
+Enrico Tassi <tassi@cs.unibo.it>
+Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
+Stefano Zacchiroli <zacchiro@cs.unibo.it>
--- /dev/null
+Copyright (C) 2000-2005, HELM Team.
+
+Matita is part of HELM, an Hypertextual, Electronic
+Library of Mathematics, developed at the Computer Science
+Department, University of Bologna, Italy.
+
+HELM is free software; you can redistribute it and/or
+modify it under the terms of the GNU General Public License
+as published by the Free Software Foundation; either version 2
+of the License, or (at your option) any later version.
+
+HELM is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with HELM; if not, write to the Free Software
+Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+MA 02111-1307, USA.
+
+For details, see the HELM World-Wide-Web page,
+http://helm.cs.unibo.it/
<glade-interface>
-<widget class="GtkDialog" id="AboutWin">
- <property name="title" translatable="yes">Matita: about</property>
- <property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_CENTER</property>
- <property name="modal">True</property>
- <property name="resizable">False</property>
- <property name="destroy_with_parent">False</property>
- <property name="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
- <property name="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox2">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area2">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
-
- <child>
- <widget class="GtkButton" id="AboutDismissButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-ok</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-5</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- <property name="pack_type">GTK_PACK_END</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkLabel" id="AboutLabel">
- <property name="visible">True</property>
- <property name="label" translatable="yes"><b>Matita @VERSION@</b>
-
-<tt>http://helm.cs.unibo.it</tt>
-
-Copyright (C) 2005,
-<i>the HELM team</i></property>
- <property name="use_underline">False</property>
- <property name="use_markup">True</property>
- <property name="justify">GTK_JUSTIFY_CENTER</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">5</property>
- <property name="ypad">5</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
- </widget>
- </child>
-</widget>
-
<widget class="GtkWindow" id="BrowserWin">
<property name="visible">True</property>
<property name="title" translatable="yes">Cic browser</property>
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
- let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
let findRepl = new findReplWin () in
let develList = new develListWin () in
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main; c findRepl]);
+ [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
*)
[ ];
(* about win *)
- ignore (about#aboutWin#event#connect#delete (fun _ -> true));
- ignore (main#aboutMenuItem#connect#activate (fun _ ->
- about#aboutWin#show ()));
- connect_button about#aboutDismissButton (fun _ ->
- about#aboutWin#misc#hide ());
- about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
- ~templ:BuildTimeConf.version about#aboutLabel#label);
+ let parse_txt_file file =
+ let ch = open_in file in
+ let l_rev = ref [] in
+ try
+ while true do
+ l_rev := input_line ch :: !l_rev;
+ done;
+ assert false
+ with
+ End_of_file ->
+ close_in ch;
+ List.rev !l_rev in
+ let about_dialog =
+ GWindow.about_dialog
+ ~authors:(parse_txt_file "AUTHORS")
+ ~comments:"comments"
+ ~copyright:"Copyright (C) 2005, the HELM team"
+ ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
+ (*?logo:GdkPixbuf.pixbuf*)
+ (*?logo_icon_name:string*)
+ ~name:"Matita"
+ ~version:BuildTimeConf.version
+ ~website:"http://helm.cs.unibo.it"
+ ()
+ in
+ ignore (main#aboutMenuItem#connect#activate
+ (fun _ -> about_dialog#present ()));
(* findRepl win *)
let show_find_Repl () =
findRepl#toplevel#misc#show ();
method console = console
method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
- method about = about
method fileSel = fileSel
method findRepl = findRepl
method main = main
(** {2 Access to singleton instances of lower-level GTK widgets} *)
- method about : MatitaGeneratedGui.aboutWin
method fileSel : MatitaGeneratedGui.fileSelectionWin
method main : MatitaGeneratedGui.mainWin
method findRepl : MatitaGeneratedGui.findReplWin
projects / helm.git / commitdiff