]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/matitaGeneratedGui.ml
Remove all traces of autoconf/automake/makefile
[helm.git] / matita / matita / matitaGeneratedGui.ml
1 (* Automatically generated from matita.ui by lablgladecc *)
2
3 let data = "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<!-- Generated with glade 3.22.1 -->\n<interface>\n  <requires lib=\"gtk+\" version=\"3.20\"/>\n  <object class=\"GtkWindow\" id=\"AutoWin\">\n    <property name=\"width_request\">600</property>\n    <property name=\"height_request\">400</property>\n    <property name=\"visible\">True</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Auto</property>\n    <property name=\"type_hint\">dialog</property>\n    <property name=\"gravity\">south-east</property>\n    <child>\n      <object class=\"GtkBox\" id=\"vbox17\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox30\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"spacing\">2</property>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindowAREA\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"shadow_type\">in</property>\n                <child>\n                  <object class=\"GtkViewport\" id=\"viewportAREA\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <child>\n                      <object class=\"GtkGrid\" id=\"table\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"vbox18\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"orientation\">vertical</property>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonUP\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <child>\n                      <object class=\"GtkAlignment\" id=\"alignment19\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"xscale\">0</property>\n                        <property name=\"yscale\">0</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"hbox31\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"spacing\">2</property>\n                            <child>\n                              <object class=\"GtkImage\" id=\"image1066\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"stock\">gtk-go-up</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                            <child>\n                              <object class=\"GtkLabel\" id=\"label30\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"use_underline\">True</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">1</property>\n                              </packing>\n                            </child>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonDOWN\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <child>\n                      <object class=\"GtkImage\" id=\"image1065\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-go-down</property>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">True</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkSeparator\" id=\"hseparator3\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"padding\">3</property>\n            <property name=\"position\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox32\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"labelLAST\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">Last:</property>\n                <property name=\"xalign\">0</property>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButtonBox\" id=\"hbuttonbox3\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"border_width\">4</property>\n                <property name=\"spacing\">4</property>\n                <property name=\"layout_style\">end</property>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonPAUSE\">\n                    <property name=\"label\">gtk-media-pause</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonPLAY\">\n                    <property name=\"label\">gtk-media-play</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonNEXT\">\n                    <property name=\"label\">gtk-media-next</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">2</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonCLOSE\">\n                    <property name=\"label\">gtk-close</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">3</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"BrowserWin\">\n    <property name=\"width_request\">500</property>\n    <property name=\"height_request\">480</property>\n    <property name=\"visible\">True</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Cic browser</property>\n    <property name=\"window_position\">center-on-parent</property>\n    <property name=\"default_width\">500</property>\n    <property name=\"default_height\">480</property>\n    <property name=\"destroy_with_parent\">True</property>\n    <child>\n      <object class=\"GtkEventBox\" id=\"BrowserWinEventBox\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <child>\n          <object class=\"GtkBox\" id=\"BrowserVBox\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkMenuBar\" id=\"menubar2\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"BrowserFileMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_File</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"BrowserFileMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserNewMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_New</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserUrlMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Open _Location ...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"L\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separatormenuitem1\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserCloseMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Quit</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"BrowserEditMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Edit</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"BrowserEditMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserCopyMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Copy</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkFrame\" id=\"frame2\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label_xalign\">0</property>\n                <property name=\"label_yalign\">0</property>\n                <property name=\"shadow_type\">none</property>\n                <child>\n                  <object class=\"GtkBox\" id=\"BrowserHBox\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserNewButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image303\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-new</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">0</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserBackButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image304\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-go-back</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserForwardButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image305\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-go-forward</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">2</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserRefreshButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"can_default\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"tooltip_text\" translatable=\"yes\">refresh</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image229\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-refresh</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">3</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserHomeButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"can_default\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"tooltip_text\" translatable=\"yes\">home</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image190\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-home</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">4</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"image301\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-jump-to</property>\n                        <property name=\"icon_size\">2</property>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"padding\">3</property>\n                        <property name=\"position\">5</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkBox\" id=\"UriHBox\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkEntry\" id=\"browserUri\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"has_focus\">True</property>\n                            <property name=\"invisible_char\">\226\151\143</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">True</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">6</property>\n                      </packing>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkNotebook\" id=\"mathOrListNotebook\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"ScrolledBrowser\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"mathLabel\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">MathView</property>\n                  </object>\n                  <packing>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"scrolledwindow9\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"shadow_type\">in</property>\n                    <child>\n                      <object class=\"GtkTreeView\" id=\"whelpResultTreeview\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"headers_visible\">False</property>\n                        <child internal-child=\"selection\">\n                          <object class=\"GtkTreeSelection\"/>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"WhelpResult\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">WhelpResult</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">1</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"scrolledwindow11\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <child>\n                      <object class=\"GtkViewport\" id=\"viewport2\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"shadow_type\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"BrowserImage\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-missing-image</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">2</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"EasterEggLabel\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">WhelpEasterEgg</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">2</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"GraphScrolledWin\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">3</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"label26\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">Graph</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">3</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkBox\" id=\"vbox20\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"orientation\">vertical</property>\n                    <child>\n                      <object class=\"GtkScrolledWindow\" id=\"scrolledwinContent\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"border_width\">3</property>\n                        <property name=\"shadow_type\">in</property>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">True</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">0</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox35\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"border_width\">4</property>\n                        <property name=\"spacing\">4</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"vbox22\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"orientation\">vertical</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkEntry\" id=\"entrySearch\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"has_focus\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkButton\" id=\"buttonSearch\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"receives_default\">False</property>\n                            <child>\n                              <object class=\"GtkAlignment\" id=\"alignment21\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"xscale\">0</property>\n                                <property name=\"yscale\">0</property>\n                                <child>\n                                  <object class=\"GtkBox\" id=\"hbox36\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"spacing\">2</property>\n                                    <child>\n                                      <object class=\"GtkImage\" id=\"image1068\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"stock\">gtk-find</property>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"fill\">False</property>\n                                        <property name=\"position\">0</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkLabel\" id=\"label32\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Search</property>\n                                        <property name=\"use_underline\">True</property>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"fill\">False</property>\n                                        <property name=\"position\">1</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                </child>\n                              </object>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">2</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">4</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"SearchText\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">SearchText</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">4</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n          </object>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkDialog\" id=\"DisambiguationErrors\">\n    <property name=\"width_request\">450</property>\n    <property name=\"height_request\">400</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">title</property>\n    <property name=\"modal\">True</property>\n    <property name=\"type_hint\">dialog</property>\n    <child internal-child=\"vbox\">\n      <object class=\"GtkBox\" id=\"vbox14\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <child internal-child=\"action_area\">\n          <object class=\"GtkButtonBox\" id=\"hbuttonbox2\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"layout_style\">spread</property>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">False</property>\n            <property name=\"pack_type\">end</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox15\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"disambiguationErrorsLabel\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">some informative message here ...</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindow12\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"vexpand\">True</property>\n                <property name=\"shadow_type\">in</property>\n                <child>\n                  <object class=\"GtkTreeView\" id=\"treeview\">\n                    <property name=\"height_request\">717</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"headers_visible\">False</property>\n                    <child internal-child=\"selection\">\n                      <object class=\"GtkTreeSelection\"/>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"FindReplWin\">\n    <property name=\"can_focus\">False</property>\n    <property name=\"border_width\">5</property>\n    <property name=\"title\" translatable=\"yes\">Find &amp; Replace</property>\n    <property name=\"resizable\">False</property>\n    <property name=\"window_position\">mouse</property>\n    <property name=\"type_hint\">dialog</property>\n    <child>\n      <object class=\"GtkGrid\" id=\"table1\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"row_spacing\">9</property>\n        <child>\n          <object class=\"GtkLabel\" id=\"label17\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"label\" translatable=\"yes\">Find:</property>\n            <property name=\"xalign\">0</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkLabel\" id=\"label18\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"label\" translatable=\"yes\">Replace with: </property>\n            <property name=\"xalign\">0</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkEntry\" id=\"findEntry\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">True</property>\n            <property name=\"can_default\">True</property>\n            <property name=\"has_default\">True</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">1</property>\n            <property name=\"top_attach\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkEntry\" id=\"replaceEntry\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">True</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">1</property>\n            <property name=\"top_attach\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox19\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"spacing\">5</property>\n            <property name=\"homogeneous\">True</property>\n            <child>\n              <object class=\"GtkButton\" id=\"findButton\">\n                <property name=\"label\">gtk-find</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"findReplButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment13\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox20\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image357\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-find-and-replace</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"label19\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Replace</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"cancelButton\">\n                <property name=\"label\">gtk-cancel</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">2</property>\n            <property name=\"width\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"MainWin\">\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Matita</property>\n    <child>\n      <object class=\"GtkEventBox\" id=\"MainWinEventBox\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox8\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkMenuBar\" id=\"menubar1\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"fileMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_File</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"fileMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"newMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_New</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"n\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"openMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Open...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"o\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"saveMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Save</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"s\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"saveAsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Save as...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"s\" signal=\"activate\" modifiers=\"GDK_SHIFT_MASK | GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator2\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"closeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Close</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"w\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"quitMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Quit</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"q\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"editMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Edit</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"editMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"undoMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"sensitive\">False</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Undo</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"z\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"redoMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"sensitive\">False</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Redo</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"z\" signal=\"activate\" modifiers=\"GDK_SHIFT_MASK | GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator3\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"cutMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Cut</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"x\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"copyMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Copy</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"c\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"pasteMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Paste</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"v\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"pastePatternMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Paste as pattern</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"unicodeAsTexMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Paste Unicode as TeX</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"menuitemAutoAltL\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Auto-expand TeX Macros</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"deleteMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Delete</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator4\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"selectAllMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Select _All</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator7\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"findReplMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Find and replace...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"f\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator8\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"LigatureButton\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Next ligature</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"l\" signal=\"activate\" modifiers=\"GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"externalEditorMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Edit with e_xternal editor</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"scriptMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Script</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"scriptMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptAdvanceMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute 1 phrase</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Page_Down\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptRetractMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Retract 1 phrase</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Page_Up\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator9\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptBottomMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute all</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"End\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptTopMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Retract all</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Home\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator10\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptJumpMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute until cursor</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"period\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"viewMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_View</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"viewMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"newCicBrowserMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">New CIC _browser</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F3\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator5\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"fullscreenMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">_Fullscreen</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F11\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"menuitemPalette\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Natural deduction palette</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F2\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator1\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"increaseFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Zoom in</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"plus\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"decreaseFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Zoom out</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"minus\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"normalFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Normal size</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"equal\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator12\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"ppNotationMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Pretty print notation</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"hideCoercionsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Hide coercions</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator13\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showCoercionsGraphMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Coercions Graph</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showHintsDbMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Hints database</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showTermGrammarMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Terms grammar</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showUnicodeTable\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">TeX/UTF-8 table</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"debugMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Debug</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"debugMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator6\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"helpMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Help</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"helpMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"contentsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Contents</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F1\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"aboutMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">About</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"hbox99\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkPaned\" id=\"hpaneScriptSequent\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox18\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"TacticsButtonsHandlebox\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <child>\n                              <object class=\"GtkBox\" id=\"vboxTacticsPalette\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"orientation\">vertical</property>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander1\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox1\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butImpl_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label8\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Implication (\226\135\146&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label7\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction (\226\136\167&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_intro_left\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label9\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction left (\226\136\168&lt;sub&gt;i-l&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_intro_right\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label10\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction right (\226\136\168&lt;sub&gt;i-r&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">3</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butNot_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label11\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Negation (\194\172&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">4</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butTop_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label12\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Top (\226\138\164&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">5</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butForall_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label20\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Universal (\226\136\128&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">6</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butExists_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label21\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Existential (\226\136\131&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">7</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label4\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Introduction rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">0</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander2\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox3\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butImpl_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label22\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Implication (\226\135\146&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_elim_left\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label23\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction left (\226\136\167&lt;sub&gt;e-l&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_elim_right\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label24\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction right (\226\136\167&lt;sub&gt;e-r&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label27\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction (\226\136\168&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">3</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butNot_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label31\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Negation (\194\172&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">4</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butBot_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label33\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Bottom (\226\138\165&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">5</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butForall_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label34\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Universal (\226\136\128&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">6</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butExists_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label35\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Existential (\226\136\131&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">7</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label5\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Elimination rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">1</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander3\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox4\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butRAA\">\n                                            <property name=\"label\" translatable=\"yes\">Reduction to Absurdity (RAA)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butUseLemma\">\n                                            <property name=\"label\" translatable=\"yes\">Use lemma (lem)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butDischarge\">\n                                            <property name=\"label\" translatable=\"yes\">Discharge (discharge)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label6\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Misc rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">2</property>\n                                  </packing>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkBox\" id=\"vboxScript\">\n                            <property name=\"width_request\">400</property>\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"orientation\">vertical</property>\n                            <child>\n                              <object class=\"GtkBox\" id=\"hbox28\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <child>\n                                  <object class=\"GtkToolbar\" id=\"buttonsToolbar\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"toolbar_style\">both</property>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem41\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptTopButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Retract all</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image920\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-goto-top</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem42\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptRetractButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Retract 1 phrase</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image921\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-go-up</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem43\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptJumpButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute until cursor</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image922\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-jump-to</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem44\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptAdvanceButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute 1 phrase</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image923\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-go-down</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem45\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptBottomButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute all</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image924\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-goto-bottom</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">True</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">0</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkToolbar\" id=\"toolbar2\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"orientation\">vertical</property>\n                                    <property name=\"toolbar_style\">both</property>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem46\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptAbortButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image927\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-stop</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">1</property>\n                                  </packing>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                            <child>\n                              <object class=\"GtkNotebook\" id=\"scriptNotebook\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">True</property>\n                                <property name=\"scrollable\">True</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">True</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">1</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"resize\">False</property>\n                        <property name=\"shrink\">True</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkPaned\" id=\"vpaned1\">\n                        <property name=\"width_request\">250</property>\n                        <property name=\"height_request\">500</property>\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"orientation\">vertical</property>\n                        <property name=\"position\">380</property>\n                        <child>\n                          <object class=\"GtkNotebook\" id=\"sequentsNotebook\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"scrollable\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"resize\">False</property>\n                            <property name=\"shrink\">True</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkBox\" id=\"hbox9\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <child>\n                              <object class=\"GtkScrolledWindow\" id=\"logScrolledWin\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">True</property>\n                                <property name=\"hscrollbar_policy\">never</property>\n                                <property name=\"shadow_type\">in</property>\n                                <child>\n                                  <object class=\"GtkTextView\" id=\"logTextView\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <property name=\"editable\">False</property>\n                                    <property name=\"wrap_mode\">char</property>\n                                    <property name=\"cursor_visible\">False</property>\n                                  </object>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">True</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"resize\">True</property>\n                            <property name=\"shrink\">True</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"resize\">True</property>\n                        <property name=\"shrink\">True</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"hbox10\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkStatusbar\" id=\"StatusBar\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkNotebook\" id=\"HintNotebook\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"show_tabs\">False</property>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintLowImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label14\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label14</property>\n                      </object>\n                      <packing>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintMediumImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label15\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label15</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">1</property>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintHighImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">2</property>\n                      </packing>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label16\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label16</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">2</property>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n          </object>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkDialog\" id=\"UriChoiceDialog\">\n    <property name=\"height_request\">280</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Uri choice</property>\n    <property name=\"modal\">True</property>\n    <property name=\"window_position\">center</property>\n    <property name=\"type_hint\">dialog</property>\n    <child internal-child=\"vbox\">\n      <object class=\"GtkBox\" id=\"dialog-vbox3\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <property name=\"spacing\">4</property>\n        <child internal-child=\"action_area\">\n          <object class=\"GtkButtonBox\" id=\"dialog-action_area3\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"layout_style\">end</property>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceAbortButton\">\n                <property name=\"label\">gtk-cancel</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceSelectedButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment2\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox3\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image19\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-index</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"label3\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Try _Selected</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceConstantsButton\">\n                <property name=\"label\" translatable=\"yes\">Try Constants</property>\n                <property name=\"visible\">True</property>\n                <property name=\"sensitive\">False</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_underline\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"copyButton\">\n                <property name=\"label\">gtk-copy</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"uriChoiceAutoButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment5\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox16\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image302\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-ok</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"okLabel\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">bla bla bla</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">4</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"uriChoiceForwardButton\">\n                <property name=\"label\">gtk-go-forward</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">5</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">False</property>\n            <property name=\"pack_type\">end</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox2\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <property name=\"spacing\">3</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"UriChoiceLabel\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">some informative message here ...</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindow1\">\n                <property name=\"width_request\">400</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"vexpand\">True</property>\n                <child>\n                  <object class=\"GtkTreeView\" id=\"UriChoiceTreeView\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"headers_visible\">False</property>\n                    <child internal-child=\"selection\">\n                      <object class=\"GtkTreeSelection\"/>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"uriEntryHBox\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"vexpand\">True</property>\n                <child>\n                  <object class=\"GtkLabel\" id=\"label2\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">URI: </property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkEntry\" id=\"entry1\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n    <action-widgets>\n      <action-widget response=\"-6\">UriChoiceAbortButton</action-widget>\n    </action-widgets>\n  </object>\n</interface>\n"
4
5 class autoWin ?translation_domain () =
6  let builder = GBuilder.builder ?translation_domain () in
7  let _ = builder#add_objects_from_string data ["AutoWin"] in
8   object
9     val toplevel =
10       new GWindow.window (GtkWindow.Window.cast (builder#get_object "AutoWin"))
11     method toplevel = toplevel
12     val autoWin =
13       new GWindow.window (GtkWindow.Window.cast (builder#get_object "AutoWin"))
14     method autoWin = autoWin
15     val vbox17 =
16       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox17"))
17     method vbox17 = vbox17
18     val hbox30 =
19       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox30"))
20     method hbox30 = hbox30
21     val scrolledwindowAREA =
22       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindowAREA"))
23     method scrolledwindowAREA = scrolledwindowAREA
24     val viewportAREA =
25       new GBin.viewport (GtkBin.Viewport.cast (builder#get_object "viewportAREA"))
26     method viewportAREA = viewportAREA
27     val table =
28       new GPack.grid (GtkPack.Grid.cast (builder#get_object "table"))
29     method table = table
30     val vbox18 =
31       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox18"))
32     method vbox18 = vbox18
33     val buttonUP =
34       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonUP"))
35     method buttonUP = buttonUP
36     val alignment19 =
37       new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment19"))
38     method alignment19 = alignment19
39     val hbox31 =
40       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox31"))
41     method hbox31 = hbox31
42     val image1066 =
43       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1066"))
44     method image1066 = image1066
45     val label30 =
46       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label30"))
47     method label30 = label30
48     val buttonDOWN =
49       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonDOWN"))
50     method buttonDOWN = buttonDOWN
51     val image1065 =
52       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1065"))
53     method image1065 = image1065
54     val hseparator3 =
55       new GObj.widget_full (GtkMisc.Separator.cast (builder#get_object "hseparator3"))
56     method hseparator3 = hseparator3
57     val hbox32 =
58       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox32"))
59     method hbox32 = hbox32
60     val labelLAST =
61       new GMisc.label (GtkMisc.Label.cast (builder#get_object "labelLAST"))
62     method labelLAST = labelLAST
63     val hbuttonbox3 =
64       new GPack.button_box (GtkPack.BBox.cast (builder#get_object "hbuttonbox3"))
65     method hbuttonbox3 = hbuttonbox3
66     val buttonPAUSE =
67       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonPAUSE"))
68     method buttonPAUSE = buttonPAUSE
69     val buttonPLAY =
70       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonPLAY"))
71     method buttonPLAY = buttonPLAY
72     val buttonNEXT =
73       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonNEXT"))
74     method buttonNEXT = buttonNEXT
75     val buttonCLOSE =
76       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonCLOSE"))
77     method buttonCLOSE = buttonCLOSE
78     method reparent parent =
79       vbox17#misc#reparent parent;
80       toplevel#destroy ()
81   end
82 class browserWin ?translation_domain () =
83  let builder = GBuilder.builder ?translation_domain () in
84  let _ = builder#add_objects_from_string data ["BrowserWin"] in
85   object
86     val toplevel =
87       new GWindow.window (GtkWindow.Window.cast (builder#get_object "BrowserWin"))
88     method toplevel = toplevel
89     val browserWin =
90       new GWindow.window (GtkWindow.Window.cast (builder#get_object "BrowserWin"))
91     method browserWin = browserWin
92     val browserWinEventBox =
93       new GBin.event_box (GtkBin.EventBox.cast (builder#get_object "BrowserWinEventBox"))
94     method browserWinEventBox = browserWinEventBox
95     val browserVBox =
96       new GPack.box (GtkPack.Box.cast (builder#get_object "BrowserVBox"))
97     method browserVBox = browserVBox
98     val menubar2 =
99       new GMenu.menu_shell (GtkMenu.MenuBar.cast (builder#get_object "menubar2"))
100     method menubar2 = menubar2
101     val browserFileMenu =
102       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserFileMenu"))
103     method browserFileMenu = browserFileMenu
104     val browserFileMenu_menu =
105       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "BrowserFileMenu_menu"))
106     method browserFileMenu_menu = browserFileMenu_menu
107     val browserNewMenuItem =
108       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserNewMenuItem"))
109     method browserNewMenuItem = browserNewMenuItem
110     val browserUrlMenuItem =
111       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserUrlMenuItem"))
112     method browserUrlMenuItem = browserUrlMenuItem
113     val separatormenuitem1 =
114       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separatormenuitem1"))
115     method separatormenuitem1 = separatormenuitem1
116     val browserCloseMenuItem =
117       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserCloseMenuItem"))
118     method browserCloseMenuItem = browserCloseMenuItem
119     val browserEditMenu =
120       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserEditMenu"))
121     method browserEditMenu = browserEditMenu
122     val browserEditMenu_menu =
123       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "BrowserEditMenu_menu"))
124     method browserEditMenu_menu = browserEditMenu_menu
125     val browserCopyMenuItem =
126       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserCopyMenuItem"))
127     method browserCopyMenuItem = browserCopyMenuItem
128     val frame2 =
129       new GBin.frame (GtkBin.Frame.cast (builder#get_object "frame2"))
130     method frame2 = frame2
131     val browserHBox =
132       new GPack.box (GtkPack.Box.cast (builder#get_object "BrowserHBox"))
133     method browserHBox = browserHBox
134     val browserNewButton =
135       new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserNewButton"))
136     method browserNewButton = browserNewButton
137     val image303 =
138       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image303"))
139     method image303 = image303
140     val browserBackButton =
141       new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserBackButton"))
142     method browserBackButton = browserBackButton
143     val image304 =
144       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image304"))
145     method image304 = image304
146     val browserForwardButton =
147       new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserForwardButton"))
148     method browserForwardButton = browserForwardButton
149     val image305 =
150       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image305"))
151     method image305 = image305
152     val browserRefreshButton =
153       new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserRefreshButton"))
154     method browserRefreshButton = browserRefreshButton
155     val image229 =
156       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image229"))
157     method image229 = image229
158     val browserHomeButton =
159       new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserHomeButton"))
160     method browserHomeButton = browserHomeButton
161     val image190 =
162       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image190"))
163     method image190 = image190
164     val image301 =
165       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image301"))
166     method image301 = image301
167     val uriHBox =
168       new GPack.box (GtkPack.Box.cast (builder#get_object "UriHBox"))
169     method uriHBox = uriHBox
170     val browserUri =
171       new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "browserUri"))
172     method browserUri = browserUri
173     val mathOrListNotebook =
174       new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "mathOrListNotebook"))
175     method mathOrListNotebook = mathOrListNotebook
176     val scrolledBrowser =
177       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "ScrolledBrowser"))
178     method scrolledBrowser = scrolledBrowser
179     val mathLabel =
180       new GMisc.label (GtkMisc.Label.cast (builder#get_object "mathLabel"))
181     method mathLabel = mathLabel
182     val scrolledwindow9 =
183       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow9"))
184     method scrolledwindow9 = scrolledwindow9
185     val whelpResultTreeview =
186       new GTree.view (GtkTree.TreeView.cast (builder#get_object "whelpResultTreeview"))
187     method whelpResultTreeview = whelpResultTreeview
188     val whelpResult =
189       new GMisc.label (GtkMisc.Label.cast (builder#get_object "WhelpResult"))
190     method whelpResult = whelpResult
191     val scrolledwindow11 =
192       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow11"))
193     method scrolledwindow11 = scrolledwindow11
194     val viewport2 =
195       new GBin.viewport (GtkBin.Viewport.cast (builder#get_object "viewport2"))
196     method viewport2 = viewport2
197     val browserImage =
198       new GMisc.image (GtkMisc.Image.cast (builder#get_object "BrowserImage"))
199     method browserImage = browserImage
200     val easterEggLabel =
201       new GMisc.label (GtkMisc.Label.cast (builder#get_object "EasterEggLabel"))
202     method easterEggLabel = easterEggLabel
203     val graphScrolledWin =
204       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "GraphScrolledWin"))
205     method graphScrolledWin = graphScrolledWin
206     val label26 =
207       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label26"))
208     method label26 = label26
209     val vbox20 =
210       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox20"))
211     method vbox20 = vbox20
212     val scrolledwinContent =
213       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwinContent"))
214     method scrolledwinContent = scrolledwinContent
215     val hbox35 =
216       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox35"))
217     method hbox35 = hbox35
218     val vbox22 =
219       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox22"))
220     method vbox22 = vbox22
221     val entrySearch =
222       new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "entrySearch"))
223     method entrySearch = entrySearch
224     val buttonSearch =
225       new GButton.button (GtkButton.Button.cast (builder#get_object "buttonSearch"))
226     method buttonSearch = buttonSearch
227     val alignment21 =
228       new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment21"))
229     method alignment21 = alignment21
230     val hbox36 =
231       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox36"))
232     method hbox36 = hbox36
233     val image1068 =
234       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1068"))
235     method image1068 = image1068
236     val label32 =
237       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label32"))
238     method label32 = label32
239     val searchText =
240       new GMisc.label (GtkMisc.Label.cast (builder#get_object "SearchText"))
241     method searchText = searchText
242     method reparent parent =
243       browserWinEventBox#misc#reparent parent;
244       toplevel#destroy ()
245   end
246 class disambiguationErrors ?translation_domain () =
247  let builder = GBuilder.builder ?translation_domain () in
248  let _ = builder#add_objects_from_string data ["DisambiguationErrors"] in
249   object
250     val toplevel =
251       new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "DisambiguationErrors"))
252     method toplevel = toplevel
253     val disambiguationErrors =
254       new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "DisambiguationErrors"))
255     method disambiguationErrors = disambiguationErrors
256     val vbox14 =
257       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox14"))
258     method vbox14 = vbox14
259     val hbuttonbox2 =
260       new GPack.button_box (GtkPack.BBox.cast (builder#get_object "hbuttonbox2"))
261     method hbuttonbox2 = hbuttonbox2
262     val vbox15 =
263       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox15"))
264     method vbox15 = vbox15
265     val disambiguationErrorsLabel =
266       new GMisc.label (GtkMisc.Label.cast (builder#get_object "disambiguationErrorsLabel"))
267     method disambiguationErrorsLabel = disambiguationErrorsLabel
268     val scrolledwindow12 =
269       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow12"))
270     method scrolledwindow12 = scrolledwindow12
271     val treeview =
272       new GTree.view (GtkTree.TreeView.cast (builder#get_object "treeview"))
273     method treeview = treeview
274     method reparent parent =
275       vbox14#misc#reparent parent;
276       toplevel#destroy ()
277   end
278 class findReplWin ?translation_domain () =
279  let builder = GBuilder.builder ?translation_domain () in
280  let _ = builder#add_objects_from_string data ["FindReplWin"] in
281   object
282     val toplevel =
283       new GWindow.window (GtkWindow.Window.cast (builder#get_object "FindReplWin"))
284     method toplevel = toplevel
285     val findReplWin =
286       new GWindow.window (GtkWindow.Window.cast (builder#get_object "FindReplWin"))
287     method findReplWin = findReplWin
288     val table1 =
289       new GPack.grid (GtkPack.Grid.cast (builder#get_object "table1"))
290     method table1 = table1
291     val label17 =
292       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label17"))
293     method label17 = label17
294     val label18 =
295       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label18"))
296     method label18 = label18
297     val findEntry =
298       new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "findEntry"))
299     method findEntry = findEntry
300     val replaceEntry =
301       new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "replaceEntry"))
302     method replaceEntry = replaceEntry
303     val hbox19 =
304       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox19"))
305     method hbox19 = hbox19
306     val findButton =
307       new GButton.button (GtkButton.Button.cast (builder#get_object "findButton"))
308     method findButton = findButton
309     val findReplButton =
310       new GButton.button (GtkButton.Button.cast (builder#get_object "findReplButton"))
311     method findReplButton = findReplButton
312     val alignment13 =
313       new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment13"))
314     method alignment13 = alignment13
315     val hbox20 =
316       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox20"))
317     method hbox20 = hbox20
318     val image357 =
319       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image357"))
320     method image357 = image357
321     val label19 =
322       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label19"))
323     method label19 = label19
324     val cancelButton =
325       new GButton.button (GtkButton.Button.cast (builder#get_object "cancelButton"))
326     method cancelButton = cancelButton
327     method reparent parent =
328       table1#misc#reparent parent;
329       toplevel#destroy ()
330   end
331 class mainWin ?translation_domain () =
332  let builder = GBuilder.builder ?translation_domain () in
333  let _ = builder#add_objects_from_string data ["MainWin"] in
334   object
335     val toplevel =
336       new GWindow.window (GtkWindow.Window.cast (builder#get_object "MainWin"))
337     method toplevel = toplevel
338     val mainWin =
339       new GWindow.window (GtkWindow.Window.cast (builder#get_object "MainWin"))
340     method mainWin = mainWin
341     val mainWinEventBox =
342       new GBin.event_box (GtkBin.EventBox.cast (builder#get_object "MainWinEventBox"))
343     method mainWinEventBox = mainWinEventBox
344     val vbox8 =
345       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox8"))
346     method vbox8 = vbox8
347     val menubar1 =
348       new GMenu.menu_shell (GtkMenu.MenuBar.cast (builder#get_object "menubar1"))
349     method menubar1 = menubar1
350     val fileMenu =
351       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "fileMenu"))
352     method fileMenu = fileMenu
353     val fileMenu_menu =
354       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "fileMenu_menu"))
355     method fileMenu_menu = fileMenu_menu
356     val newMenuItem =
357       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "newMenuItem"))
358     method newMenuItem = newMenuItem
359     val openMenuItem =
360       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "openMenuItem"))
361     method openMenuItem = openMenuItem
362     val saveMenuItem =
363       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "saveMenuItem"))
364     method saveMenuItem = saveMenuItem
365     val saveAsMenuItem =
366       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "saveAsMenuItem"))
367     method saveAsMenuItem = saveAsMenuItem
368     val separator2 =
369       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator2"))
370     method separator2 = separator2
371     val closeMenuItem =
372       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "closeMenuItem"))
373     method closeMenuItem = closeMenuItem
374     val quitMenuItem =
375       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "quitMenuItem"))
376     method quitMenuItem = quitMenuItem
377     val editMenu =
378       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "editMenu"))
379     method editMenu = editMenu
380     val editMenu_menu =
381       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "editMenu_menu"))
382     method editMenu_menu = editMenu_menu
383     val undoMenuItem =
384       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "undoMenuItem"))
385     method undoMenuItem = undoMenuItem
386     val redoMenuItem =
387       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "redoMenuItem"))
388     method redoMenuItem = redoMenuItem
389     val separator3 =
390       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator3"))
391     method separator3 = separator3
392     val cutMenuItem =
393       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "cutMenuItem"))
394     method cutMenuItem = cutMenuItem
395     val copyMenuItem =
396       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "copyMenuItem"))
397     method copyMenuItem = copyMenuItem
398     val pasteMenuItem =
399       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "pasteMenuItem"))
400     method pasteMenuItem = pasteMenuItem
401     val pastePatternMenuItem =
402       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "pastePatternMenuItem"))
403     method pastePatternMenuItem = pastePatternMenuItem
404     val unicodeAsTexMenuItem =
405       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "unicodeAsTexMenuItem"))
406     method unicodeAsTexMenuItem = unicodeAsTexMenuItem
407     val menuitemAutoAltL =
408       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "menuitemAutoAltL"))
409     method menuitemAutoAltL = menuitemAutoAltL
410     val deleteMenuItem =
411       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "deleteMenuItem"))
412     method deleteMenuItem = deleteMenuItem
413     val separator4 =
414       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator4"))
415     method separator4 = separator4
416     val selectAllMenuItem =
417       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "selectAllMenuItem"))
418     method selectAllMenuItem = selectAllMenuItem
419     val separator7 =
420       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator7"))
421     method separator7 = separator7
422     val findReplMenuItem =
423       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "findReplMenuItem"))
424     method findReplMenuItem = findReplMenuItem
425     val separator8 =
426       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator8"))
427     method separator8 = separator8
428     val ligatureButton =
429       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "LigatureButton"))
430     method ligatureButton = ligatureButton
431     val externalEditorMenuItem =
432       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "externalEditorMenuItem"))
433     method externalEditorMenuItem = externalEditorMenuItem
434     val scriptMenu =
435       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptMenu"))
436     method scriptMenu = scriptMenu
437     val scriptMenu_menu =
438       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "scriptMenu_menu"))
439     method scriptMenu_menu = scriptMenu_menu
440     val scriptAdvanceMenuItem =
441       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptAdvanceMenuItem"))
442     method scriptAdvanceMenuItem = scriptAdvanceMenuItem
443     val scriptRetractMenuItem =
444       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptRetractMenuItem"))
445     method scriptRetractMenuItem = scriptRetractMenuItem
446     val separator9 =
447       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator9"))
448     method separator9 = separator9
449     val scriptBottomMenuItem =
450       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptBottomMenuItem"))
451     method scriptBottomMenuItem = scriptBottomMenuItem
452     val scriptTopMenuItem =
453       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptTopMenuItem"))
454     method scriptTopMenuItem = scriptTopMenuItem
455     val separator10 =
456       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator10"))
457     method separator10 = separator10
458     val scriptJumpMenuItem =
459       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptJumpMenuItem"))
460     method scriptJumpMenuItem = scriptJumpMenuItem
461     val viewMenu =
462       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "viewMenu"))
463     method viewMenu = viewMenu
464     val viewMenu_menu =
465       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "viewMenu_menu"))
466     method viewMenu_menu = viewMenu_menu
467     val newCicBrowserMenuItem =
468       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "newCicBrowserMenuItem"))
469     method newCicBrowserMenuItem = newCicBrowserMenuItem
470     val separator5 =
471       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator5"))
472     method separator5 = separator5
473     val fullscreenMenuItem =
474       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "fullscreenMenuItem"))
475     method fullscreenMenuItem = fullscreenMenuItem
476     val menuitemPalette =
477       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "menuitemPalette"))
478     method menuitemPalette = menuitemPalette
479     val separator1 =
480       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator1"))
481     method separator1 = separator1
482     val increaseFontSizeMenuItem =
483       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "increaseFontSizeMenuItem"))
484     method increaseFontSizeMenuItem = increaseFontSizeMenuItem
485     val decreaseFontSizeMenuItem =
486       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "decreaseFontSizeMenuItem"))
487     method decreaseFontSizeMenuItem = decreaseFontSizeMenuItem
488     val normalFontSizeMenuItem =
489       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "normalFontSizeMenuItem"))
490     method normalFontSizeMenuItem = normalFontSizeMenuItem
491     val separator12 =
492       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator12"))
493     method separator12 = separator12
494     val ppNotationMenuItem =
495       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "ppNotationMenuItem"))
496     method ppNotationMenuItem = ppNotationMenuItem
497     val hideCoercionsMenuItem =
498       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "hideCoercionsMenuItem"))
499     method hideCoercionsMenuItem = hideCoercionsMenuItem
500     val separator13 =
501       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator13"))
502     method separator13 = separator13
503     val showCoercionsGraphMenuItem =
504       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showCoercionsGraphMenuItem"))
505     method showCoercionsGraphMenuItem = showCoercionsGraphMenuItem
506     val showHintsDbMenuItem =
507       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showHintsDbMenuItem"))
508     method showHintsDbMenuItem = showHintsDbMenuItem
509     val showTermGrammarMenuItem =
510       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showTermGrammarMenuItem"))
511     method showTermGrammarMenuItem = showTermGrammarMenuItem
512     val showUnicodeTable =
513       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showUnicodeTable"))
514     method showUnicodeTable = showUnicodeTable
515     val debugMenu =
516       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "debugMenu"))
517     method debugMenu = debugMenu
518     val debugMenu_menu =
519       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "debugMenu_menu"))
520     method debugMenu_menu = debugMenu_menu
521     val separator6 =
522       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator6"))
523     method separator6 = separator6
524     val helpMenu =
525       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "helpMenu"))
526     method helpMenu = helpMenu
527     val helpMenu_menu =
528       new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "helpMenu_menu"))
529     method helpMenu_menu = helpMenu_menu
530     val contentsMenuItem =
531       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "contentsMenuItem"))
532     method contentsMenuItem = contentsMenuItem
533     val aboutMenuItem =
534       new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "aboutMenuItem"))
535     method aboutMenuItem = aboutMenuItem
536     val hbox99 =
537       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox99"))
538     method hbox99 = hbox99
539     val hpaneScriptSequent =
540       new GPack.paned (GtkPack.Paned.cast (builder#get_object "hpaneScriptSequent"))
541     method hpaneScriptSequent = hpaneScriptSequent
542     val hbox18 =
543       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox18"))
544     method hbox18 = hbox18
545     val tacticsButtonsHandlebox =
546       new GPack.box (GtkPack.Box.cast (builder#get_object "TacticsButtonsHandlebox"))
547     method tacticsButtonsHandlebox = tacticsButtonsHandlebox
548     val vboxTacticsPalette =
549       new GPack.box (GtkPack.Box.cast (builder#get_object "vboxTacticsPalette"))
550     method vboxTacticsPalette = vboxTacticsPalette
551     val expander1 =
552       new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander1"))
553     method expander1 = expander1
554     val vbox1 =
555       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox1"))
556     method vbox1 = vbox1
557     val butImpl_intro =
558       new GButton.button (GtkButton.Button.cast (builder#get_object "butImpl_intro"))
559     method butImpl_intro = butImpl_intro
560     val label8 =
561       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label8"))
562     method label8 = label8
563     val butAnd_intro =
564       new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_intro"))
565     method butAnd_intro = butAnd_intro
566     val label7 =
567       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label7"))
568     method label7 = label7
569     val butOr_intro_left =
570       new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_intro_left"))
571     method butOr_intro_left = butOr_intro_left
572     val label9 =
573       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label9"))
574     method label9 = label9
575     val butOr_intro_right =
576       new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_intro_right"))
577     method butOr_intro_right = butOr_intro_right
578     val label10 =
579       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label10"))
580     method label10 = label10
581     val butNot_intro =
582       new GButton.button (GtkButton.Button.cast (builder#get_object "butNot_intro"))
583     method butNot_intro = butNot_intro
584     val label11 =
585       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label11"))
586     method label11 = label11
587     val butTop_intro =
588       new GButton.button (GtkButton.Button.cast (builder#get_object "butTop_intro"))
589     method butTop_intro = butTop_intro
590     val label12 =
591       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label12"))
592     method label12 = label12
593     val butForall_intro =
594       new GButton.button (GtkButton.Button.cast (builder#get_object "butForall_intro"))
595     method butForall_intro = butForall_intro
596     val label20 =
597       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label20"))
598     method label20 = label20
599     val butExists_intro =
600       new GButton.button (GtkButton.Button.cast (builder#get_object "butExists_intro"))
601     method butExists_intro = butExists_intro
602     val label21 =
603       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label21"))
604     method label21 = label21
605     val label4 =
606       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label4"))
607     method label4 = label4
608     val expander2 =
609       new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander2"))
610     method expander2 = expander2
611     val vbox3 =
612       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox3"))
613     method vbox3 = vbox3
614     val butImpl_elim =
615       new GButton.button (GtkButton.Button.cast (builder#get_object "butImpl_elim"))
616     method butImpl_elim = butImpl_elim
617     val label22 =
618       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label22"))
619     method label22 = label22
620     val butAnd_elim_left =
621       new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_elim_left"))
622     method butAnd_elim_left = butAnd_elim_left
623     val label23 =
624       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label23"))
625     method label23 = label23
626     val butAnd_elim_right =
627       new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_elim_right"))
628     method butAnd_elim_right = butAnd_elim_right
629     val label24 =
630       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label24"))
631     method label24 = label24
632     val butOr_elim =
633       new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_elim"))
634     method butOr_elim = butOr_elim
635     val label27 =
636       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label27"))
637     method label27 = label27
638     val butNot_elim =
639       new GButton.button (GtkButton.Button.cast (builder#get_object "butNot_elim"))
640     method butNot_elim = butNot_elim
641     val label31 =
642       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label31"))
643     method label31 = label31
644     val butBot_elim =
645       new GButton.button (GtkButton.Button.cast (builder#get_object "butBot_elim"))
646     method butBot_elim = butBot_elim
647     val label33 =
648       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label33"))
649     method label33 = label33
650     val butForall_elim =
651       new GButton.button (GtkButton.Button.cast (builder#get_object "butForall_elim"))
652     method butForall_elim = butForall_elim
653     val label34 =
654       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label34"))
655     method label34 = label34
656     val butExists_elim =
657       new GButton.button (GtkButton.Button.cast (builder#get_object "butExists_elim"))
658     method butExists_elim = butExists_elim
659     val label35 =
660       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label35"))
661     method label35 = label35
662     val label5 =
663       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label5"))
664     method label5 = label5
665     val expander3 =
666       new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander3"))
667     method expander3 = expander3
668     val vbox4 =
669       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox4"))
670     method vbox4 = vbox4
671     val butRAA =
672       new GButton.button (GtkButton.Button.cast (builder#get_object "butRAA"))
673     method butRAA = butRAA
674     val butUseLemma =
675       new GButton.button (GtkButton.Button.cast (builder#get_object "butUseLemma"))
676     method butUseLemma = butUseLemma
677     val butDischarge =
678       new GButton.button (GtkButton.Button.cast (builder#get_object "butDischarge"))
679     method butDischarge = butDischarge
680     val label6 =
681       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label6"))
682     method label6 = label6
683     val vboxScript =
684       new GPack.box (GtkPack.Box.cast (builder#get_object "vboxScript"))
685     method vboxScript = vboxScript
686     val hbox28 =
687       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox28"))
688     method hbox28 = hbox28
689     val buttonsToolbar =
690       new GButton.toolbar (GtkButton.Toolbar.cast (builder#get_object "buttonsToolbar"))
691     method buttonsToolbar = buttonsToolbar
692     val toolitem41 =
693       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem41"))
694     method toolitem41 = toolitem41
695     val scriptTopButton =
696       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptTopButton"))
697     method scriptTopButton = scriptTopButton
698     val image920 =
699       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image920"))
700     method image920 = image920
701     val toolitem42 =
702       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem42"))
703     method toolitem42 = toolitem42
704     val scriptRetractButton =
705       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptRetractButton"))
706     method scriptRetractButton = scriptRetractButton
707     val image921 =
708       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image921"))
709     method image921 = image921
710     val toolitem43 =
711       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem43"))
712     method toolitem43 = toolitem43
713     val scriptJumpButton =
714       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptJumpButton"))
715     method scriptJumpButton = scriptJumpButton
716     val image922 =
717       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image922"))
718     method image922 = image922
719     val toolitem44 =
720       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem44"))
721     method toolitem44 = toolitem44
722     val scriptAdvanceButton =
723       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptAdvanceButton"))
724     method scriptAdvanceButton = scriptAdvanceButton
725     val image923 =
726       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image923"))
727     method image923 = image923
728     val toolitem45 =
729       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem45"))
730     method toolitem45 = toolitem45
731     val scriptBottomButton =
732       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptBottomButton"))
733     method scriptBottomButton = scriptBottomButton
734     val image924 =
735       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image924"))
736     method image924 = image924
737     val toolbar2 =
738       new GButton.toolbar (GtkButton.Toolbar.cast (builder#get_object "toolbar2"))
739     method toolbar2 = toolbar2
740     val toolitem46 =
741       new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem46"))
742     method toolitem46 = toolitem46
743     val scriptAbortButton =
744       new GButton.button (GtkButton.Button.cast (builder#get_object "scriptAbortButton"))
745     method scriptAbortButton = scriptAbortButton
746     val image927 =
747       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image927"))
748     method image927 = image927
749     val scriptNotebook =
750       new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "scriptNotebook"))
751     method scriptNotebook = scriptNotebook
752     val vpaned1 =
753       new GPack.paned (GtkPack.Paned.cast (builder#get_object "vpaned1"))
754     method vpaned1 = vpaned1
755     val sequentsNotebook =
756       new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "sequentsNotebook"))
757     method sequentsNotebook = sequentsNotebook
758     val hbox9 =
759       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox9"))
760     method hbox9 = hbox9
761     val logScrolledWin =
762       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "logScrolledWin"))
763     method logScrolledWin = logScrolledWin
764     val logTextView =
765       new GText.view (GtkText.View.cast (builder#get_object "logTextView"))
766     method logTextView = logTextView
767     val hbox10 =
768       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox10"))
769     method hbox10 = hbox10
770     val statusBar =
771       new GMisc.statusbar (GtkMisc.Statusbar.cast (builder#get_object "StatusBar"))
772     method statusBar = statusBar
773     val hintNotebook =
774       new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "HintNotebook"))
775     method hintNotebook = hintNotebook
776     val hintLowImage =
777       new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintLowImage"))
778     method hintLowImage = hintLowImage
779     val label14 =
780       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label14"))
781     method label14 = label14
782     val hintMediumImage =
783       new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintMediumImage"))
784     method hintMediumImage = hintMediumImage
785     val label15 =
786       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label15"))
787     method label15 = label15
788     val hintHighImage =
789       new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintHighImage"))
790     method hintHighImage = hintHighImage
791     val label16 =
792       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label16"))
793     method label16 = label16
794     method reparent parent =
795       mainWinEventBox#misc#reparent parent;
796       toplevel#destroy ()
797   end
798 class uriChoiceDialog ?translation_domain () =
799  let builder = GBuilder.builder ?translation_domain () in
800  let _ = builder#add_objects_from_string data ["UriChoiceDialog"] in
801   object
802     val toplevel =
803       new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "UriChoiceDialog"))
804     method toplevel = toplevel
805     val uriChoiceDialog =
806       new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "UriChoiceDialog"))
807     method uriChoiceDialog = uriChoiceDialog
808     val dialog_vbox3 =
809       new GPack.box (GtkPack.Box.cast (builder#get_object "dialog-vbox3"))
810     method dialog_vbox3 = dialog_vbox3
811     val dialog_action_area3 =
812       new GPack.button_box (GtkPack.BBox.cast (builder#get_object "dialog-action_area3"))
813     method dialog_action_area3 = dialog_action_area3
814     val uriChoiceAbortButton =
815       new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceAbortButton"))
816     method uriChoiceAbortButton = uriChoiceAbortButton
817     val uriChoiceSelectedButton =
818       new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceSelectedButton"))
819     method uriChoiceSelectedButton = uriChoiceSelectedButton
820     val alignment2 =
821       new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment2"))
822     method alignment2 = alignment2
823     val hbox3 =
824       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox3"))
825     method hbox3 = hbox3
826     val image19 =
827       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image19"))
828     method image19 = image19
829     val label3 =
830       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label3"))
831     method label3 = label3
832     val uriChoiceConstantsButton =
833       new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceConstantsButton"))
834     method uriChoiceConstantsButton = uriChoiceConstantsButton
835     val copyButton =
836       new GButton.button (GtkButton.Button.cast (builder#get_object "copyButton"))
837     method copyButton = copyButton
838     val uriChoiceAutoButton =
839       new GButton.button (GtkButton.Button.cast (builder#get_object "uriChoiceAutoButton"))
840     method uriChoiceAutoButton = uriChoiceAutoButton
841     val alignment5 =
842       new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment5"))
843     method alignment5 = alignment5
844     val hbox16 =
845       new GPack.box (GtkPack.Box.cast (builder#get_object "hbox16"))
846     method hbox16 = hbox16
847     val image302 =
848       new GMisc.image (GtkMisc.Image.cast (builder#get_object "image302"))
849     method image302 = image302
850     val okLabel =
851       new GMisc.label (GtkMisc.Label.cast (builder#get_object "okLabel"))
852     method okLabel = okLabel
853     val uriChoiceForwardButton =
854       new GButton.button (GtkButton.Button.cast (builder#get_object "uriChoiceForwardButton"))
855     method uriChoiceForwardButton = uriChoiceForwardButton
856     val vbox2 =
857       new GPack.box (GtkPack.Box.cast (builder#get_object "vbox2"))
858     method vbox2 = vbox2
859     val uriChoiceLabel =
860       new GMisc.label (GtkMisc.Label.cast (builder#get_object "UriChoiceLabel"))
861     method uriChoiceLabel = uriChoiceLabel
862     val scrolledwindow1 =
863       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow1"))
864     method scrolledwindow1 = scrolledwindow1
865     val uriChoiceTreeView =
866       new GTree.view (GtkTree.TreeView.cast (builder#get_object "UriChoiceTreeView"))
867     method uriChoiceTreeView = uriChoiceTreeView
868     val uriEntryHBox =
869       new GPack.box (GtkPack.Box.cast (builder#get_object "uriEntryHBox"))
870     method uriEntryHBox = uriEntryHBox
871     val label2 =
872       new GMisc.label (GtkMisc.Label.cast (builder#get_object "label2"))
873     method label2 = label2
874     val entry1 =
875       new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "entry1"))
876     method entry1 = entry1
877     method reparent parent =
878       dialog_vbox3#misc#reparent parent;
879       toplevel#destroy ()
880   end