moved matita logo in the right place

diff --git a/helm/matita/icons/matita.png b/helm/matita/icons/matita.png
new file mode 100644 (file)
index 0000000..342bcb4
Binary files /dev/null and b/helm/matita/icons/matita.png differ

diff --git a/helm/matita/icons/matita_medium.png b/helm/matita/icons/matita_medium.png
new file mode 100644 (file)
index 0000000..335688a
Binary files /dev/null and b/helm/matita/icons/matita_medium.png differ

diff --git a/helm/matita/icons/matita_small.png b/helm/matita/icons/matita_small.png
new file mode 100644 (file)
index 0000000..cfb017b
Binary files /dev/null and b/helm/matita/icons/matita_small.png differ

diff --git a/helm/matita/icons/meegg.png b/helm/matita/icons/meegg.png
new file mode 100644 (file)
index 0000000..4c2be73
Binary files /dev/null and b/helm/matita/icons/meegg.png differ

diff --git a/helm/matita/logo/matita.png b/helm/matita/logo/matita.png
deleted file mode 100644 (file)
index 342bcb4..0000000
Binary files a/helm/matita/logo/matita.png and /dev/null differ

diff --git a/helm/matita/logo/matita_medium.png b/helm/matita/logo/matita_medium.png
deleted file mode 100644 (file)
index 335688a..0000000
Binary files a/helm/matita/logo/matita_medium.png and /dev/null differ

diff --git a/helm/matita/logo/matita_small.png b/helm/matita/logo/matita_small.png
deleted file mode 100644 (file)
index cfb017b..0000000
Binary files a/helm/matita/logo/matita_small.png and /dev/null differ

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 1076b9192f57993f4d96c180457783607b6a84da..9c40b8efa2d0c99bd89777b014a7c4bc4580b081 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -18,6 +18,7 @@
   <property name="skip_pager_hint">False</property>
   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkEventBox" id="BrowserWinEventBox">
@@ -347,6 +348,10 @@
                  <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>
@@ -370,6 +375,9 @@
                      <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>
@@ -392,6 +400,47 @@
                  <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>
+
+             <child>
+               <widget class="GtkImage" id="EasterEggImage">
+                 <property name="visible">True</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xpad">0</property>
+                 <property name="ypad">0</property>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkLabel" id="EasterEggLabel">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">WhelpEasterEgg</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>
@@ -422,6 +471,7 @@
   <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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -482,6 +532,10 @@
          <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="padding">0</property>
@@ -506,6 +560,7 @@
   <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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -566,6 +621,10 @@
          <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="padding">0</property>
@@ -594,6 +653,7 @@
   <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="focus_on_map">True</property>
   <property name="show_fileops">True</property>
 
   <child internal-child="cancel_button">
@@ -631,6 +691,7 @@
   <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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -710,6 +771,10 @@
              <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="padding">0</property>
@@ -735,6 +800,9 @@
                  <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>
@@ -767,6 +835,7 @@
   <property name="skip_pager_hint">False</property>
   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkEventBox" id="MainWinEventBox">
@@ -2163,6 +2232,10 @@
                                  <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>
@@ -2186,6 +2259,9 @@
                                      <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>
@@ -2208,6 +2284,10 @@
                                  <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>
@@ -2380,6 +2460,10 @@
                      <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>
@@ -2413,6 +2497,10 @@
                      <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>
@@ -2446,6 +2534,10 @@
                      <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>
@@ -2483,6 +2575,7 @@
   <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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -2543,6 +2636,10 @@
          <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="padding">0</property>
@@ -2603,6 +2700,7 @@
   <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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -2686,6 +2784,10 @@
                          <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="padding">0</property>
@@ -2783,6 +2885,10 @@
                          <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="padding">0</property>
@@ -2824,6 +2930,10 @@
              <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="padding">0</property>
@@ -2850,6 +2960,9 @@
                  <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>
@@ -2879,6 +2992,10 @@
                  <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="padding">0</property>
@@ -2936,6 +3053,7 @@
   <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="focus_on_map">True</property>
 
   <child>
     <widget class="GtkTable" id="table1">
@@ -2959,6 +3077,10 @@
          <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="left_attach">0</property>
@@ -2983,6 +3105,10 @@
          <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="left_attach">0</property>
@@ -3137,6 +3263,10 @@
                          <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="padding">0</property>
@@ -3196,6 +3326,7 @@
   <property name="skip_pager_hint">False</property>
   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkVBox" id="vbox10">
@@ -3226,6 +3357,10 @@
              <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="left_attach">0</property>
@@ -3250,6 +3385,10 @@
              <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="left_attach">0</property>
@@ -3422,6 +3561,7 @@
   <property name="skip_pager_hint">False</property>
   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkVBox" id="vbox12">
@@ -3446,6 +3586,9 @@
              <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>
@@ -3582,6 +3725,10 @@
                          <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="padding">0</property>
@@ -3656,6 +3803,10 @@
                          <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="padding">0</property>

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 1b46c03a4e2ea4b678564b503ad21fa35b889cf0..a3d35c8e1129081de4c82de57706350f23b3cb74 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -171,9 +171,7 @@ class gui () =
         (*~comments:"comments"*)
         ~copyright:"Copyright (C) 2005, the HELM team"
         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
-        ~logo:
-          (GdkPixbuf.from_file
-            (BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png"))
+        ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
         ~name:"Matita"
         ~version:BuildTimeConf.version
         ~website:"http://helm.cs.unibo.it"

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 532c3dd975a3a2fe4d1364dca912273a51562fd0..43547b8ff9e835da80e588d3c1efdd8db659c1bb 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -404,11 +404,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable scrolledWin: GBin.scrolled_window option = None
       (* scrolled window to which the sequentViewer is currently attached *)
     val logo = (GMisc.image
-      ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") ()
+      ~file:(MatitaMisc.image_path "matita_medium.png") ()
       :> GObj.widget)
             
     val logo_with_qed = (GMisc.image
-      ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+      ~file:(MatitaMisc.image_path "matita_small.png") ()
       :> GObj.widget)
 
     method load_logo =
@@ -593,6 +593,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     with exn -> fail (MatitaExcPp.to_string exn)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
+  let load_easter_egg = lazy (
+    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
   object (self)
     inherit scriptAccessor
     
@@ -682,9 +685,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
      * 
      * Use only these functions to switch between the tabs
      *)
-    method private _showList = win#mathOrListNotebook#goto_page 1
     method private _showMath = win#mathOrListNotebook#goto_page 0
-    
+    method private _showList = win#mathOrListNotebook#goto_page 1
+
     method private back () =
       try
         self#_load (self#_historyPrev ())
@@ -704,7 +707,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
-          | `About `Us -> () (* TODO implement easter egg here :-] *)
+          | `About `Us -> self#egg ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -725,6 +728,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       failwith "not implemented _loadCheck";
       self#_showMath
 
+    method private egg () =
+      win#mathOrListNotebook#goto_page 2;
+      Lazy.force load_easter_egg
+
     method private home () =
       self#_showMath;
       match self#script#status.proof_status with