helm/software/matita/matita.glade

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE glade-interface SYSTEM "glade-2.0.dtd">
   3 <!--*- mode: xml -*-->
   4 <glade-interface>
   5   <widget class="GtkWindow" id="BrowserWin">
   6     <property name="width_request">640</property>
   7     <property name="height_request">480</property>
   8     <property name="visible">True</property>
   9     <property name="title" translatable="yes">Cic browser</property>
  10     <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
  11     <property name="default_width">640</property>
  12     <property name="default_height">480</property>
  13     <property name="destroy_with_parent">True</property>
  14     <property name="transient_for">MainWin</property>
  15     <child>
  16       <widget class="GtkEventBox" id="BrowserWinEventBox">
  17         <property name="visible">True</property>
  18         <child>
  19           <widget class="GtkVBox" id="BrowserVBox">
  20             <property name="visible">True</property>
  21             <child>
  22               <widget class="GtkMenuBar" id="menubar2">
  23                 <property name="visible">True</property>
  24                 <child>
  25                   <widget class="GtkMenuItem" id="BrowserFileMenu">
  26                     <property name="visible">True</property>
  27                     <property name="label" translatable="yes">_File</property>
  28                     <property name="use_underline">True</property>
  29                     <child>
  30                       <widget class="GtkMenu" id="BrowserFileMenu_menu">
  31                         <child>
  32                           <widget class="GtkImageMenuItem" id="BrowserNewMenuItem">
  33                             <property name="visible">True</property>
  34                             <property name="label">gtk-new</property>
  35                             <property name="use_underline">True</property>
  36                             <property name="use_stock">True</property>
  37                           </widget>
  38                         </child>
  39                         <child>
  40                           <widget class="GtkMenuItem" id="BrowserUrlMenuItem">
  41                             <property name="visible">True</property>
  42                             <property name="label" translatable="yes">Open _Location ...</property>
  43                             <property name="use_underline">True</property>
  44                             <accelerator key="L" modifiers="GDK_CONTROL_MASK" signal="activate"/>
  45                           </widget>
  46                         </child>
  47                         <child>
  48                           <widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
  49                             <property name="visible">True</property>
  50                           </widget>
  51                         </child>
  52                         <child>
  53                           <widget class="GtkImageMenuItem" id="BrowserCloseMenuItem">
  54                             <property name="visible">True</property>
  55                             <property name="label">gtk-close</property>
  56                             <property name="use_underline">True</property>
  57                             <property name="use_stock">True</property>
  58                           </widget>
  59                         </child>
  60                       </widget>
  61                     </child>
  62                   </widget>
  63                 </child>
  64                 <child>
  65                   <widget class="GtkMenuItem" id="BrowserEditMenu">
  66                     <property name="visible">True</property>
  67                     <property name="label" translatable="yes">_Edit</property>
  68                     <property name="use_underline">True</property>
  69                     <child>
  70                       <widget class="GtkMenu" id="BrowserEditMenu_menu">
  71                         <child>
  72                           <widget class="GtkImageMenuItem" id="BrowserCopyMenuItem">
  73                             <property name="visible">True</property>
  74                             <property name="label">gtk-copy</property>
  75                             <property name="use_underline">True</property>
  76                             <property name="use_stock">True</property>
  77                           </widget>
  78                         </child>
  79                       </widget>
  80                     </child>
  81                   </widget>
  82                 </child>
  83                 <child>
  84                   <widget class="GtkMenuItem" id="BrowserViewMenu">
  85                     <property name="visible">True</property>
  86                     <property name="label" translatable="yes">_View</property>
  87                     <property name="use_underline">True</property>
  88                     <child>
  89                       <widget class="GtkMenu" id="BrowserViewMenu_menu">
  90                         <child>
  91                           <widget class="GtkMenuItem" id="DepGraphMenuItem">
  92                             <property name="visible">True</property>
  93                             <property name="tooltip" translatable="yes">View the graph of objects on which the current one depends on</property>
  94                             <property name="label" translatable="yes">(Direct) Dependencies</property>
  95                             <property name="use_underline">True</property>
  96                           </widget>
  97                         </child>
  98                         <child>
  99                           <widget class="GtkMenuItem" id="InvDepGraphMenuItem">
 100                             <property name="visible">True</property>
 101                             <property name="tooltip" translatable="yes">View the graph of objects which depends on the current one</property>
 102                             <property name="label" translatable="yes">(Inverse) Dependencies</property>
 103                             <property name="use_underline">True</property>
 104                           </widget>
 105                         </child>
 106                         <child>
 107                           <widget class="GtkMenuItem" id="univMenuItem">
 108                             <property name="visible">True</property>
 109                             <property name="label" translatable="yes">Universes</property>
 110                             <property name="use_underline">True</property>
 111                           </widget>
 112                         </child>
 113                         <child>
 114                           <widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
 115                             <property name="visible">True</property>
 116                             <property name="label" translatable="yes">HBugs Tutors</property>
 117                             <property name="use_underline">True</property>
 118                           </widget>
 119                         </child>
 120                       </widget>
 121                     </child>
 122                   </widget>
 123                 </child>
 124               </widget>
 125               <packing>
 126                 <property name="expand">False</property>
 127                 <property name="fill">False</property>
 128               </packing>
 129             </child>
 130             <child>
 131               <widget class="GtkFrame" id="frame2">
 132                 <property name="visible">True</property>
 133                 <property name="label_xalign">0</property>
 134                 <property name="label_yalign">0</property>
 135                 <property name="shadow_type">GTK_SHADOW_NONE</property>
 136                 <child>
 137                   <widget class="GtkHBox" id="BrowserHBox">
 138                     <property name="visible">True</property>
 139                     <child>
 140                       <widget class="GtkButton" id="BrowserNewButton">
 141                         <property name="visible">True</property>
 142                         <property name="can_focus">True</property>
 143                         <property name="relief">GTK_RELIEF_NONE</property>
 144                         <property name="response_id">0</property>
 145                         <child>
 146                           <widget class="GtkImage" id="image303">
 147                             <property name="visible">True</property>
 148                             <property name="stock">gtk-new</property>
 149                           </widget>
 150                         </child>
 151                       </widget>
 152                       <packing>
 153                         <property name="expand">False</property>
 154                         <property name="fill">False</property>
 155                       </packing>
 156                     </child>
 157                     <child>
 158                       <widget class="GtkButton" id="BrowserBackButton">
 159                         <property name="visible">True</property>
 160                         <property name="can_focus">True</property>
 161                         <property name="relief">GTK_RELIEF_NONE</property>
 162                         <property name="response_id">0</property>
 163                         <child>
 164                           <widget class="GtkImage" id="image304">
 165                             <property name="visible">True</property>
 166                             <property name="stock">gtk-go-back</property>
 167                           </widget>
 168                         </child>
 169                       </widget>
 170                       <packing>
 171                         <property name="expand">False</property>
 172                         <property name="fill">False</property>
 173                         <property name="position">1</property>
 174                       </packing>
 175                     </child>
 176                     <child>
 177                       <widget class="GtkButton" id="BrowserForwardButton">
 178                         <property name="visible">True</property>
 179                         <property name="can_focus">True</property>
 180                         <property name="relief">GTK_RELIEF_NONE</property>
 181                         <property name="response_id">0</property>
 182                         <child>
 183                           <widget class="GtkImage" id="image305">
 184                             <property name="visible">True</property>
 185                             <property name="stock">gtk-go-forward</property>
 186                           </widget>
 187                         </child>
 188                       </widget>
 189                       <packing>
 190                         <property name="expand">False</property>
 191                         <property name="fill">False</property>
 192                         <property name="position">2</property>
 193                       </packing>
 194                     </child>
 195                     <child>
 196                       <widget class="GtkButton" id="BrowserRefreshButton">
 197                         <property name="visible">True</property>
 198                         <property name="can_focus">True</property>
 199                         <property name="can_default">True</property>
 200                         <property name="tooltip" translatable="yes">refresh</property>
 201                         <property name="relief">GTK_RELIEF_NONE</property>
 202                         <property name="response_id">0</property>
 203                         <child>
 204                           <widget class="GtkImage" id="image229">
 205                             <property name="visible">True</property>
 206                             <property name="stock">gtk-refresh</property>
 207                           </widget>
 208                         </child>
 209                       </widget>
 210                       <packing>
 211                         <property name="expand">False</property>
 212                         <property name="fill">False</property>
 213                         <property name="position">3</property>
 214                       </packing>
 215                     </child>
 216                     <child>
 217                       <widget class="GtkButton" id="BrowserHomeButton">
 218                         <property name="visible">True</property>
 219                         <property name="can_focus">True</property>
 220                         <property name="can_default">True</property>
 221                         <property name="tooltip" translatable="yes">home</property>
 222                         <property name="relief">GTK_RELIEF_NONE</property>
 223                         <property name="response_id">0</property>
 224                         <child>
 225                           <widget class="GtkImage" id="image190">
 226                             <property name="visible">True</property>
 227                             <property name="stock">gtk-home</property>
 228                           </widget>
 229                         </child>
 230                       </widget>
 231                       <packing>
 232                         <property name="expand">False</property>
 233                         <property name="fill">False</property>
 234                         <property name="position">4</property>
 235                       </packing>
 236                     </child>
 237                     <child>
 238                       <widget class="GtkImage" id="image301">
 239                         <property name="visible">True</property>
 240                         <property name="stock">gtk-jump-to</property>
 241                         <property name="icon_size">2</property>
 242                       </widget>
 243                       <packing>
 244                         <property name="expand">False</property>
 245                         <property name="fill">False</property>
 246                         <property name="padding">3</property>
 247                         <property name="position">5</property>
 248                       </packing>
 249                     </child>
 250                     <child>
 251                       <widget class="GtkHBox" id="UriHBox">
 252                         <property name="visible">True</property>
 253                         <child>
 254                           <placeholder/>
 255                         </child>
 256                       </widget>
 257                       <packing>
 258                         <property name="position">6</property>
 259                       </packing>
 260                     </child>
 261                   </widget>
 262                 </child>
 263               </widget>
 264               <packing>
 265                 <property name="expand">False</property>
 266                 <property name="position">1</property>
 267               </packing>
 268             </child>
 269             <child>
 270               <widget class="GtkHBox" id="whelpBarBox">
 271                 <property name="visible">True</property>
 272                 <property name="border_width">3</property>
 273                 <property name="spacing">6</property>
 274                 <child>
 275                   <widget class="GtkImage" id="WhelpBarImage">
 276                     <property name="visible">True</property>
 277                     <property name="stock">gtk-missing-image</property>
 278                   </widget>
 279                   <packing>
 280                     <property name="expand">False</property>
 281                   </packing>
 282                 </child>
 283                 <child>
 284                   <widget class="GtkEntry" id="queryInputText">
 285                     <property name="visible">True</property>
 286                     <property name="can_focus">True</property>
 287                     <property name="invisible_char">*</property>
 288                   </widget>
 289                   <packing>
 290                     <property name="position">1</property>
 291                   </packing>
 292                 </child>
 293                 <child>
 294                   <widget class="GtkVBox" id="whelpBarComboVbox">
 295                     <property name="visible">True</property>
 296                     <child>
 297                       <widget class="GtkAlignment" id="alignment4">
 298                         <property name="visible">True</property>
 299                         <child>
 300                           <placeholder/>
 301                         </child>
 302                       </widget>
 303                       <packing>
 304                         <property name="expand">False</property>
 305                         <property name="fill">False</property>
 306                       </packing>
 307                     </child>
 308                   </widget>
 309                   <packing>
 310                     <property name="expand">False</property>
 311                     <property name="position">2</property>
 312                   </packing>
 313                 </child>
 314               </widget>
 315               <packing>
 316                 <property name="expand">False</property>
 317                 <property name="position">2</property>
 318               </packing>
 319             </child>
 320             <child>
 321               <widget class="GtkNotebook" id="mathOrListNotebook">
 322                 <property name="visible">True</property>
 323                 <property name="can_focus">True</property>
 324                 <child>
 325                   <widget class="GtkScrolledWindow" id="ScrolledBrowser">
 326                     <property name="visible">True</property>
 327                     <property name="can_focus">True</property>
 328                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 329                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 330                     <child>
 331                       <placeholder/>
 332                     </child>
 333                   </widget>
 334                 </child>
 335                 <child>
 336                   <widget class="GtkLabel" id="mathLabel">
 337                     <property name="visible">True</property>
 338                     <property name="label" translatable="yes">MathView</property>
 339                   </widget>
 340                   <packing>
 341                     <property name="type">tab</property>
 342                     <property name="tab_fill">False</property>
 343                   </packing>
 344                 </child>
 345                 <child>
 346                   <widget class="GtkScrolledWindow" id="scrolledwindow9">
 347                     <property name="visible">True</property>
 348                     <property name="can_focus">True</property>
 349                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 350                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 351                     <property name="shadow_type">GTK_SHADOW_IN</property>
 352                     <child>
 353                       <widget class="GtkTreeView" id="whelpResultTreeview">
 354                         <property name="visible">True</property>
 355                         <property name="can_focus">True</property>
 356                         <property name="headers_visible">False</property>
 357                       </widget>
 358                     </child>
 359                   </widget>
 360                   <packing>
 361                     <property name="position">1</property>
 362                   </packing>
 363                 </child>
 364                 <child>
 365                   <widget class="GtkLabel" id="listLabel">
 366                     <property name="visible">True</property>
 367                     <property name="label" translatable="yes">WhelpResults</property>
 368                   </widget>
 369                   <packing>
 370                     <property name="type">tab</property>
 371                     <property name="position">1</property>
 372                     <property name="tab_fill">False</property>
 373                   </packing>
 374                 </child>
 375                 <child>
 376                   <widget class="GtkScrolledWindow" id="scrolledwindow11">
 377                     <property name="visible">True</property>
 378                     <property name="can_focus">True</property>
 379                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 380                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 381                     <child>
 382                       <widget class="GtkViewport" id="viewport2">
 383                         <property name="visible">True</property>
 384                         <property name="shadow_type">GTK_SHADOW_NONE</property>
 385                         <child>
 386                           <widget class="GtkImage" id="BrowserImage">
 387                             <property name="visible">True</property>
 388                             <property name="stock">gtk-missing-image</property>
 389                           </widget>
 390                         </child>
 391                       </widget>
 392                     </child>
 393                   </widget>
 394                   <packing>
 395                     <property name="position">2</property>
 396                   </packing>
 397                 </child>
 398                 <child>
 399                   <widget class="GtkLabel" id="EasterEggLabel">
 400                     <property name="visible">True</property>
 401                     <property name="label" translatable="yes">WhelpEasterEgg</property>
 402                   </widget>
 403                   <packing>
 404                     <property name="type">tab</property>
 405                     <property name="position">2</property>
 406                     <property name="tab_fill">False</property>
 407                   </packing>
 408                 </child>
 409                 <child>
 410                   <widget class="GtkScrolledWindow" id="GraphScrolledWin">
 411                     <property name="visible">True</property>
 412                     <property name="can_focus">True</property>
 413                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 414                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 415                     <child>
 416                       <placeholder/>
 417                     </child>
 418                   </widget>
 419                   <packing>
 420                     <property name="position">3</property>
 421                   </packing>
 422                 </child>
 423                 <child>
 424                   <widget class="GtkLabel" id="label26">
 425                     <property name="visible">True</property>
 426                     <property name="label" translatable="yes">Graph</property>
 427                   </widget>
 428                   <packing>
 429                     <property name="type">tab</property>
 430                     <property name="position">3</property>
 431                     <property name="tab_fill">False</property>
 432                   </packing>
 433                 </child>
 434                 <child>
 435                   <widget class="GtkVBox" id="vbox16">
 436                     <property name="visible">True</property>
 437                     <child>
 438                       <widget class="GtkScrolledWindow" id="scrolledwindow13">
 439                         <property name="visible">True</property>
 440                         <property name="can_focus">True</property>
 441                         <child>
 442                           <widget class="GtkTreeView" id="HBugsTutorsList">
 443                             <property name="visible">True</property>
 444                             <property name="can_focus">True</property>
 445                           </widget>
 446                         </child>
 447                       </widget>
 448                     </child>
 449                     <child>
 450                       <widget class="GtkToolbar" id="toolbar3">
 451                         <property name="visible">True</property>
 452                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 453                         <child>
 454                           <widget class="GtkToolItem" id="toolitem47">
 455                             <property name="visible">True</property>
 456                             <child>
 457                               <widget class="GtkButton" id="HBugsRefreshButton">
 458                                 <property name="visible">True</property>
 459                                 <property name="can_focus">True</property>
 460                                 <property name="label">gtk-refresh</property>
 461                                 <property name="use_stock">True</property>
 462                                 <property name="response_id">0</property>
 463                               </widget>
 464                             </child>
 465                           </widget>
 466                           <packing>
 467                             <property name="expand">False</property>
 468                             <property name="homogeneous">False</property>
 469                           </packing>
 470                         </child>
 471                         <child>
 472                           <widget class="GtkToolItem" id="toolitem48">
 473                             <property name="visible">True</property>
 474                             <child>
 475                               <widget class="GtkButton" id="HBugsUnsubscribeButton">
 476                                 <property name="visible">True</property>
 477                                 <property name="can_focus">True</property>
 478                                 <property name="label">gtk-remove</property>
 479                                 <property name="use_stock">True</property>
 480                                 <property name="response_id">0</property>
 481                               </widget>
 482                             </child>
 483                           </widget>
 484                           <packing>
 485                             <property name="expand">False</property>
 486                             <property name="homogeneous">False</property>
 487                           </packing>
 488                         </child>
 489                         <child>
 490                           <widget class="GtkToolItem" id="toolitem49">
 491                             <property name="visible">True</property>
 492                             <child>
 493                               <widget class="GtkButton" id="HBugsSubscribeButton">
 494                                 <property name="visible">True</property>
 495                                 <property name="can_focus">True</property>
 496                                 <property name="label">gtk-add</property>
 497                                 <property name="use_stock">True</property>
 498                                 <property name="response_id">0</property>
 499                               </widget>
 500                             </child>
 501                           </widget>
 502                           <packing>
 503                             <property name="expand">False</property>
 504                             <property name="homogeneous">False</property>
 505                           </packing>
 506                         </child>
 507                       </widget>
 508                       <packing>
 509                         <property name="expand">False</property>
 510                         <property name="fill">False</property>
 511                         <property name="position">1</property>
 512                       </packing>
 513                     </child>
 514                   </widget>
 515                   <packing>
 516                     <property name="position">4</property>
 517                   </packing>
 518                 </child>
 519                 <child>
 520                   <widget class="GtkLabel" id="label29">
 521                     <property name="visible">True</property>
 522                     <property name="label" translatable="yes">HBugs</property>
 523                   </widget>
 524                   <packing>
 525                     <property name="type">tab</property>
 526                     <property name="position">4</property>
 527                     <property name="tab_fill">False</property>
 528                   </packing>
 529                 </child>
 530                 <child>
 531                   <widget class="GtkScrolledWindow" id="textScrolledWin">
 532                     <property name="visible">True</property>
 533                     <property name="can_focus">True</property>
 534                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 535                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 536                     <child>
 537                       <widget class="GtkTreeView" id="universesTreeview">
 538                         <property name="visible">True</property>
 539                         <property name="can_focus">True</property>
 540                       </widget>
 541                     </child>
 542                   </widget>
 543                   <packing>
 544                     <property name="position">5</property>
 545                   </packing>
 546                 </child>
 547                 <child>
 548                   <widget class="GtkLabel" id="universes">
 549                     <property name="visible">True</property>
 550                     <property name="label" translatable="yes">Universes</property>
 551                   </widget>
 552                   <packing>
 553                     <property name="type">tab</property>
 554                     <property name="position">5</property>
 555                     <property name="tab_fill">False</property>
 556                   </packing>
 557                 </child>
 558                 <child>
 559                   <widget class="GtkVBox" id="vbox20">
 560                     <property name="visible">True</property>
 561                     <child>
 562                       <widget class="GtkScrolledWindow" id="scrolledwinContent">
 563                         <property name="visible">True</property>
 564                         <property name="can_focus">True</property>
 565                         <property name="border_width">3</property>
 566                         <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 567                         <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 568                         <property name="shadow_type">GTK_SHADOW_IN</property>
 569                         <child>
 570                           <placeholder/>
 571                         </child>
 572                       </widget>
 573                     </child>
 574                     <child>
 575                       <widget class="GtkHBox" id="hbox35">
 576                         <property name="visible">True</property>
 577                         <property name="border_width">4</property>
 578                         <property name="spacing">4</property>
 579                         <child>
 580                           <widget class="GtkVBox" id="vbox22">
 581                             <property name="visible">True</property>
 582                             <child>
 583                               <placeholder/>
 584                             </child>
 585                             <child>
 586                               <placeholder/>
 587                             </child>
 588                           </widget>
 589                         </child>
 590                         <child>
 591                           <widget class="GtkEntry" id="entrySearch">
 592                             <property name="visible">True</property>
 593                             <property name="can_focus">True</property>
 594                           </widget>
 595                           <packing>
 596                             <property name="position">1</property>
 597                           </packing>
 598                         </child>
 599                         <child>
 600                           <widget class="GtkButton" id="buttonSearch">
 601                             <property name="visible">True</property>
 602                             <property name="can_focus">True</property>
 603                             <property name="response_id">0</property>
 604                             <child>
 605                               <widget class="GtkAlignment" id="alignment21">
 606                                 <property name="visible">True</property>
 607                                 <property name="xscale">0</property>
 608                                 <property name="yscale">0</property>
 609                                 <child>
 610                                   <widget class="GtkHBox" id="hbox36">
 611                                     <property name="visible">True</property>
 612                                     <property name="spacing">2</property>
 613                                     <child>
 614                                       <widget class="GtkImage" id="image1068">
 615                                         <property name="visible">True</property>
 616                                         <property name="stock">gtk-find</property>
 617                                       </widget>
 618                                       <packing>
 619                                         <property name="expand">False</property>
 620                                         <property name="fill">False</property>
 621                                       </packing>
 622                                     </child>
 623                                     <child>
 624                                       <widget class="GtkLabel" id="label32">
 625                                         <property name="visible">True</property>
 626                                         <property name="label" translatable="yes">Search</property>
 627                                         <property name="use_underline">True</property>
 628                                       </widget>
 629                                       <packing>
 630                                         <property name="expand">False</property>
 631                                         <property name="fill">False</property>
 632                                         <property name="position">1</property>
 633                                       </packing>
 634                                     </child>
 635                                   </widget>
 636                                 </child>
 637                               </widget>
 638                             </child>
 639                           </widget>
 640                           <packing>
 641                             <property name="expand">False</property>
 642                             <property name="fill">False</property>
 643                             <property name="position">2</property>
 644                           </packing>
 645                         </child>
 646                       </widget>
 647                       <packing>
 648                         <property name="expand">False</property>
 649                         <property name="position">1</property>
 650                       </packing>
 651                     </child>
 652                   </widget>
 653                   <packing>
 654                     <property name="position">6</property>
 655                   </packing>
 656                 </child>
 657                 <child>
 658                   <widget class="GtkLabel" id="label1">
 659                     <property name="visible">True</property>
 660                     <property name="label" translatable="yes">SearchText</property>
 661                   </widget>
 662                   <packing>
 663                     <property name="type">tab</property>
 664                     <property name="position">6</property>
 665                     <property name="tab_fill">False</property>
 666                   </packing>
 667                 </child>
 668               </widget>
 669               <packing>
 670                 <property name="position">3</property>
 671               </packing>
 672             </child>
 673           </widget>
 674         </child>
 675       </widget>
 676     </child>
 677   </widget>
 678   <widget class="GtkDialog" id="ConfirmationDialog">
 679     <property name="title" translatable="yes">DUMMY</property>
 680     <property name="resizable">False</property>
 681     <property name="modal">True</property>
 682     <property name="window_position">GTK_WIN_POS_CENTER</property>
 683     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 684     <child internal-child="vbox">
 685       <widget class="GtkVBox" id="dialog-vbox1">
 686         <property name="visible">True</property>
 687         <child>
 688           <widget class="GtkLabel" id="ConfirmationDialogLabel">
 689             <property name="visible">True</property>
 690             <property name="label" translatable="yes">DUMMY</property>
 691             <property name="justify">GTK_JUSTIFY_CENTER</property>
 692           </widget>
 693           <packing>
 694             <property name="expand">False</property>
 695             <property name="fill">False</property>
 696             <property name="position">2</property>
 697           </packing>
 698         </child>
 699         <child internal-child="action_area">
 700           <widget class="GtkHButtonBox" id="dialog-action_area1">
 701             <property name="visible">True</property>
 702             <property name="layout_style">GTK_BUTTONBOX_END</property>
 703             <child>
 704               <widget class="GtkButton" id="ConfirmationDialogCancelButton">
 705                 <property name="visible">True</property>
 706                 <property name="can_focus">True</property>
 707                 <property name="can_default">True</property>
 708                 <property name="label">gtk-cancel</property>
 709                 <property name="use_stock">True</property>
 710                 <property name="response_id">-6</property>
 711               </widget>
 712             </child>
 713             <child>
 714               <widget class="GtkButton" id="ConfirmationDialogOkButton">
 715                 <property name="visible">True</property>
 716                 <property name="can_focus">True</property>
 717                 <property name="can_default">True</property>
 718                 <property name="label">gtk-ok</property>
 719                 <property name="use_stock">True</property>
 720                 <property name="response_id">-5</property>
 721               </widget>
 722               <packing>
 723                 <property name="position">1</property>
 724               </packing>
 725             </child>
 726           </widget>
 727           <packing>
 728             <property name="expand">False</property>
 729             <property name="pack_type">GTK_PACK_END</property>
 730           </packing>
 731         </child>
 732       </widget>
 733     </child>
 734   </widget>
 735   <widget class="GtkDialog" id="EmptyDialog">
 736     <property name="visible">True</property>
 737     <property name="title" translatable="yes">DUMMY</property>
 738     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 739     <child internal-child="vbox">
 740       <widget class="GtkVBox" id="EmptyDialogVBox">
 741         <property name="visible">True</property>
 742         <child>
 743           <widget class="GtkLabel" id="EmptyDialogLabel">
 744             <property name="visible">True</property>
 745             <property name="label" translatable="yes">DUMMY</property>
 746           </widget>
 747           <packing>
 748             <property name="expand">False</property>
 749             <property name="fill">False</property>
 750             <property name="position">2</property>
 751           </packing>
 752         </child>
 753         <child>
 754           <placeholder/>
 755         </child>
 756         <child internal-child="action_area">
 757           <widget class="GtkHButtonBox" id="dialog-action_area5">
 758             <property name="visible">True</property>
 759             <property name="layout_style">GTK_BUTTONBOX_END</property>
 760             <child>
 761               <widget class="GtkButton" id="EmptyDialogCancelButton">
 762                 <property name="visible">True</property>
 763                 <property name="can_focus">True</property>
 764                 <property name="can_default">True</property>
 765                 <property name="label">gtk-cancel</property>
 766                 <property name="use_stock">True</property>
 767                 <property name="response_id">-6</property>
 768               </widget>
 769             </child>
 770             <child>
 771               <widget class="GtkButton" id="EmptyDialogOkButton">
 772                 <property name="visible">True</property>
 773                 <property name="can_focus">True</property>
 774                 <property name="can_default">True</property>
 775                 <property name="label">gtk-ok</property>
 776                 <property name="use_stock">True</property>
 777                 <property name="response_id">-5</property>
 778               </widget>
 779               <packing>
 780                 <property name="position">1</property>
 781               </packing>
 782             </child>
 783           </widget>
 784           <packing>
 785             <property name="expand">False</property>
 786             <property name="pack_type">GTK_PACK_END</property>
 787           </packing>
 788         </child>
 789       </widget>
 790     </child>
 791   </widget>
 792   <widget class="GtkFileSelection" id="FileSelectionWin">
 793     <property name="border_width">10</property>
 794     <property name="title" translatable="yes">Select File</property>
 795     <property name="modal">True</property>
 796     <property name="window_position">GTK_WIN_POS_CENTER</property>
 797     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 798     <property name="show_fileops">True</property>
 799     <child internal-child="cancel_button">
 800       <widget class="GtkButton" id="fileSelCancelButton">
 801         <property name="visible">True</property>
 802         <property name="can_focus">True</property>
 803         <property name="can_default">True</property>
 804         <property name="response_id">0</property>
 805       </widget>
 806     </child>
 807     <child internal-child="ok_button">
 808       <widget class="GtkButton" id="fileSelOkButton">
 809         <property name="visible">True</property>
 810         <property name="can_focus">True</property>
 811         <property name="can_default">True</property>
 812         <property name="response_id">0</property>
 813       </widget>
 814     </child>
 815   </widget>
 816   <widget class="GtkWindow" id="MainWin">
 817     <property name="title" translatable="yes">Matita</property>
 818     <child>
 819       <widget class="GtkEventBox" id="MainWinEventBox">
 820         <property name="visible">True</property>
 821         <child>
 822           <widget class="GtkVBox" id="vbox8">
 823             <property name="visible">True</property>
 824             <child>
 825               <widget class="GtkHandleBox" id="menuBarHandleBox">
 826                 <property name="visible">True</property>
 827                 <property name="shadow_type">GTK_SHADOW_OUT</property>
 828                 <child>
 829                   <widget class="GtkMenuBar" id="menubar1">
 830                     <property name="visible">True</property>
 831                     <child>
 832                       <widget class="GtkMenuItem" id="fileMenu">
 833                         <property name="visible">True</property>
 834                         <property name="label" translatable="yes">_File</property>
 835                         <property name="use_underline">True</property>
 836                         <child>
 837                           <widget class="GtkMenu" id="fileMenu_menu">
 838                             <child>
 839                               <widget class="GtkImageMenuItem" id="newMenuItem">
 840                                 <property name="visible">True</property>
 841                                 <property name="label" translatable="yes">_New</property>
 842                                 <property name="use_underline">True</property>
 843                                 <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 844                                 <child internal-child="image">
 845                                   <widget class="GtkImage" id="image1047">
 846                                     <property name="visible">True</property>
 847                                     <property name="stock">gtk-new</property>
 848                                     <property name="icon_size">1</property>
 849                                   </widget>
 850                                 </child>
 851                               </widget>
 852                             </child>
 853                             <child>
 854                               <widget class="GtkImageMenuItem" id="openMenuItem">
 855                                 <property name="visible">True</property>
 856                                 <property name="label" translatable="yes">_Open...</property>
 857                                 <property name="use_underline">True</property>
 858                                 <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 859                                 <child internal-child="image">
 860                                   <widget class="GtkImage" id="image1048">
 861                                     <property name="visible">True</property>
 862                                     <property name="stock">gtk-open</property>
 863                                     <property name="icon_size">1</property>
 864                                   </widget>
 865                                 </child>
 866                               </widget>
 867                             </child>
 868                             <child>
 869                               <widget class="GtkImageMenuItem" id="saveMenuItem">
 870                                 <property name="visible">True</property>
 871                                 <property name="label" translatable="yes">_Save</property>
 872                                 <property name="use_underline">True</property>
 873                                 <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 874                                 <child internal-child="image">
 875                                   <widget class="GtkImage" id="image1049">
 876                                     <property name="visible">True</property>
 877                                     <property name="stock">gtk-save</property>
 878                                     <property name="icon_size">1</property>
 879                                   </widget>
 880                                 </child>
 881                               </widget>
 882                             </child>
 883                             <child>
 884                               <widget class="GtkImageMenuItem" id="saveAsMenuItem">
 885                                 <property name="visible">True</property>
 886                                 <property name="label" translatable="yes">Save _as ...</property>
 887                                 <property name="use_underline">True</property>
 888                                 <accelerator key="s" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
 889                                 <child internal-child="image">
 890                                   <widget class="GtkImage" id="image1050">
 891                                     <property name="visible">True</property>
 892                                     <property name="stock">gtk-save-as</property>
 893                                     <property name="icon_size">1</property>
 894                                   </widget>
 895                                 </child>
 896                               </widget>
 897                             </child>
 898                             <child>
 899                               <widget class="GtkSeparatorMenuItem" id="separator2">
 900                                 <property name="visible">True</property>
 901                               </widget>
 902                             </child>
 903                             <child>
 904                               <widget class="GtkImageMenuItem" id="quitMenuItem">
 905                                 <property name="visible">True</property>
 906                                 <property name="label" translatable="yes">_Quit</property>
 907                                 <property name="use_underline">True</property>
 908                                 <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 909                                 <child internal-child="image">
 910                                   <widget class="GtkImage" id="image1052">
 911                                     <property name="visible">True</property>
 912                                     <property name="stock">gtk-quit</property>
 913                                     <property name="icon_size">1</property>
 914                                   </widget>
 915                                 </child>
 916                               </widget>
 917                             </child>
 918                           </widget>
 919                         </child>
 920                       </widget>
 921                     </child>
 922                     <child>
 923                       <widget class="GtkMenuItem" id="editMenu">
 924                         <property name="visible">True</property>
 925                         <property name="label" translatable="yes">_Edit</property>
 926                         <property name="use_underline">True</property>
 927                         <child>
 928                           <widget class="GtkMenu" id="editMenu_menu">
 929                             <child>
 930                               <widget class="GtkImageMenuItem" id="undoMenuItem">
 931                                 <property name="visible">True</property>
 932                                 <property name="sensitive">False</property>
 933                                 <property name="label" translatable="yes">_Undo</property>
 934                                 <property name="use_underline">True</property>
 935                                 <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 936                                 <child internal-child="image">
 937                                   <widget class="GtkImage" id="image1053">
 938                                     <property name="visible">True</property>
 939                                     <property name="stock">gtk-undo</property>
 940                                     <property name="icon_size">1</property>
 941                                   </widget>
 942                                 </child>
 943                               </widget>
 944                             </child>
 945                             <child>
 946                               <widget class="GtkImageMenuItem" id="redoMenuItem">
 947                                 <property name="visible">True</property>
 948                                 <property name="sensitive">False</property>
 949                                 <property name="label" translatable="yes">_Redo</property>
 950                                 <property name="use_underline">True</property>
 951                                 <accelerator key="z" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
 952                                 <child internal-child="image">
 953                                   <widget class="GtkImage" id="image1054">
 954                                     <property name="visible">True</property>
 955                                     <property name="stock">gtk-redo</property>
 956                                     <property name="icon_size">1</property>
 957                                   </widget>
 958                                 </child>
 959                               </widget>
 960                             </child>
 961                             <child>
 962                               <widget class="GtkSeparatorMenuItem" id="separator3">
 963                                 <property name="visible">True</property>
 964                               </widget>
 965                             </child>
 966                             <child>
 967                               <widget class="GtkImageMenuItem" id="cutMenuItem">
 968                                 <property name="visible">True</property>
 969                                 <property name="label" translatable="yes">Cu_t</property>
 970                                 <property name="use_underline">True</property>
 971                                 <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 972                                 <child internal-child="image">
 973                                   <widget class="GtkImage" id="image1055">
 974                                     <property name="visible">True</property>
 975                                     <property name="stock">gtk-cut</property>
 976                                     <property name="icon_size">1</property>
 977                                   </widget>
 978                                 </child>
 979                               </widget>
 980                             </child>
 981                             <child>
 982                               <widget class="GtkImageMenuItem" id="copyMenuItem">
 983                                 <property name="visible">True</property>
 984                                 <property name="label" translatable="yes">_Copy</property>
 985                                 <property name="use_underline">True</property>
 986                                 <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 987                                 <child internal-child="image">
 988                                   <widget class="GtkImage" id="image1056">
 989                                     <property name="visible">True</property>
 990                                     <property name="stock">gtk-copy</property>
 991                                     <property name="icon_size">1</property>
 992                                   </widget>
 993                                 </child>
 994                               </widget>
 995                             </child>
 996                             <child>
 997                               <widget class="GtkImageMenuItem" id="pasteMenuItem">
 998                                 <property name="visible">True</property>
 999                                 <property name="label" translatable="yes">_Paste</property>
1000                                 <property name="use_underline">True</property>
1001                                 <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1002                                 <child internal-child="image">
1003                                   <widget class="GtkImage" id="image1057">
1004                                     <property name="visible">True</property>
1005                                     <property name="stock">gtk-paste</property>
1006                                     <property name="icon_size">1</property>
1007                                   </widget>
1008                                 </child>
1009                               </widget>
1010                             </child>
1011                             <child>
1012                               <widget class="GtkMenuItem" id="pastePatternMenuItem">
1013                                 <property name="visible">True</property>
1014                                 <property name="label" translatable="yes">Paste as pattern</property>
1015                                 <property name="use_underline">True</property>
1016                               </widget>
1017                             </child>
1018                             <child>
1019                               <widget class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
1020                                 <property name="visible">True</property>
1021                                 <property name="label" translatable="yes">Paste Unicode as TeX</property>
1022                                 <property name="use_underline">True</property>
1023                               </widget>
1024                             </child>
1025                             <child>
1026                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
1027                                 <property name="visible">True</property>
1028                                 <property name="label" translatable="yes">_Delete</property>
1029                                 <property name="use_underline">True</property>
1030                                 <child internal-child="image">
1031                                   <widget class="GtkImage" id="image1058">
1032                                     <property name="visible">True</property>
1033                                     <property name="stock">gtk-delete</property>
1034                                     <property name="icon_size">1</property>
1035                                   </widget>
1036                                 </child>
1037                               </widget>
1038                             </child>
1039                             <child>
1040                               <widget class="GtkSeparatorMenuItem" id="separator4">
1041                                 <property name="visible">True</property>
1042                               </widget>
1043                             </child>
1044                             <child>
1045                               <widget class="GtkMenuItem" id="selectAllMenuItem">
1046                                 <property name="visible">True</property>
1047                                 <property name="label" translatable="yes">Select _All</property>
1048                                 <property name="use_underline">True</property>
1049                               </widget>
1050                             </child>
1051                             <child>
1052                               <widget class="GtkSeparatorMenuItem" id="separator7">
1053                                 <property name="visible">True</property>
1054                               </widget>
1055                             </child>
1056                             <child>
1057                               <widget class="GtkImageMenuItem" id="findReplMenuItem">
1058                                 <property name="visible">True</property>
1059                                 <property name="label" translatable="yes">_Find &amp; replace ...</property>
1060                                 <property name="use_underline">True</property>
1061                                 <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1062                                 <child internal-child="image">
1063                                   <widget class="GtkImage" id="image1059">
1064                                     <property name="visible">True</property>
1065                                     <property name="stock">gtk-find-and-replace</property>
1066                                     <property name="icon_size">1</property>
1067                                   </widget>
1068                                 </child>
1069                               </widget>
1070                             </child>
1071                             <child>
1072                               <widget class="GtkSeparatorMenuItem" id="separator8">
1073                                 <property name="visible">True</property>
1074                               </widget>
1075                             </child>
1076                             <child>
1077                               <widget class="GtkMenuItem" id="LigatureButton">
1078                                 <property name="visible">True</property>
1079                                 <property name="label" translatable="yes">Next ligature</property>
1080                                 <property name="use_underline">True</property>
1081                                 <accelerator key="l" modifiers="GDK_MOD1_MASK" signal="activate"/>
1082                               </widget>
1083                             </child>
1084                             <child>
1085                               <widget class="GtkMenuItem" id="externalEditorMenuItem">
1086                                 <property name="visible">True</property>
1087                                 <property name="label" translatable="yes">Edit with e_xternal editor</property>
1088                                 <property name="use_underline">True</property>
1089                               </widget>
1090                             </child>
1091                           </widget>
1092                         </child>
1093                       </widget>
1094                     </child>
1095                     <child>
1096                       <widget class="GtkMenuItem" id="scriptMenu">
1097                         <property name="visible">True</property>
1098                         <property name="label" translatable="yes">_Script</property>
1099                         <property name="use_underline">True</property>
1100                         <child>
1101                           <widget class="GtkMenu" id="scriptMenu_menu">
1102                             <child>
1103                               <widget class="GtkMenuItem" id="scriptAdvanceMenuItem">
1104                                 <property name="visible">True</property>
1105                                 <property name="label" translatable="yes">Execute 1 phrase</property>
1106                                 <property name="use_underline">True</property>
1107                                 <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1108                               </widget>
1109                             </child>
1110                             <child>
1111                               <widget class="GtkMenuItem" id="scriptRetractMenuItem">
1112                                 <property name="visible">True</property>
1113                                 <property name="label" translatable="yes">Retract 1 phrase</property>
1114                                 <property name="use_underline">True</property>
1115                                 <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1116                               </widget>
1117                             </child>
1118                             <child>
1119                               <widget class="GtkSeparatorMenuItem" id="separator9">
1120                                 <property name="visible">True</property>
1121                               </widget>
1122                             </child>
1123                             <child>
1124                               <widget class="GtkMenuItem" id="scriptBottomMenuItem">
1125                                 <property name="visible">True</property>
1126                                 <property name="label" translatable="yes">Execute all</property>
1127                                 <property name="use_underline">True</property>
1128                                 <accelerator key="End" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1129                               </widget>
1130                             </child>
1131                             <child>
1132                               <widget class="GtkMenuItem" id="scriptTopMenuItem">
1133                                 <property name="visible">True</property>
1134                                 <property name="label" translatable="yes">Restart</property>
1135                                 <property name="use_underline">True</property>
1136                                 <accelerator key="Home" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1137                               </widget>
1138                             </child>
1139                             <child>
1140                               <widget class="GtkSeparatorMenuItem" id="separator10">
1141                                 <property name="visible">True</property>
1142                               </widget>
1143                             </child>
1144                             <child>
1145                               <widget class="GtkMenuItem" id="scriptJumpMenuItem">
1146                                 <property name="visible">True</property>
1147                                 <property name="label" translatable="yes">Execute until cursor</property>
1148                                 <property name="use_underline">True</property>
1149                                 <accelerator key="period" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1150                               </widget>
1151                             </child>
1152                           </widget>
1153                         </child>
1154                       </widget>
1155                     </child>
1156                     <child>
1157                       <widget class="GtkMenuItem" id="viewMenu">
1158                         <property name="visible">True</property>
1159                         <property name="label" translatable="yes">_View</property>
1160                         <property name="use_underline">True</property>
1161                         <child>
1162                           <widget class="GtkMenu" id="viewMenu_menu">
1163                             <child>
1164                               <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
1165                                 <property name="visible">True</property>
1166                                 <property name="label" translatable="yes">Show _tactics bar</property>
1167                                 <property name="use_underline">True</property>
1168                                 <property name="active">True</property>
1169                                 <accelerator key="F2" modifiers="" signal="activate"/>
1170                               </widget>
1171                             </child>
1172                             <child>
1173                               <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1174                                 <property name="visible">True</property>
1175                                 <property name="label" translatable="yes">New CIC _browser</property>
1176                                 <property name="use_underline">True</property>
1177                                 <accelerator key="F3" modifiers="" signal="activate"/>
1178                               </widget>
1179                             </child>
1180                             <child>
1181                               <widget class="GtkSeparatorMenuItem" id="separator5">
1182                                 <property name="visible">True</property>
1183                               </widget>
1184                             </child>
1185                             <child>
1186                               <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1187                                 <property name="visible">True</property>
1188                                 <property name="label" translatable="yes">_Fullscreen</property>
1189                                 <property name="use_underline">True</property>
1190                                 <accelerator key="F11" modifiers="" signal="activate"/>
1191                               </widget>
1192                             </child>
1193                             <child>
1194                               <widget class="GtkSeparatorMenuItem" id="separator1">
1195                                 <property name="visible">True</property>
1196                               </widget>
1197                             </child>
1198                             <child>
1199                               <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
1200                                 <property name="visible">True</property>
1201                                 <property name="label" translatable="yes">Zoom _in</property>
1202                                 <property name="use_underline">True</property>
1203                                 <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1204                                 <child internal-child="image">
1205                                   <widget class="GtkImage" id="image1060">
1206                                     <property name="visible">True</property>
1207                                     <property name="stock">gtk-zoom-in</property>
1208                                     <property name="icon_size">1</property>
1209                                   </widget>
1210                                 </child>
1211                               </widget>
1212                             </child>
1213                             <child>
1214                               <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
1215                                 <property name="visible">True</property>
1216                                 <property name="label" translatable="yes">Zoom _out</property>
1217                                 <property name="use_underline">True</property>
1218                                 <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1219                                 <child internal-child="image">
1220                                   <widget class="GtkImage" id="image1061">
1221                                     <property name="visible">True</property>
1222                                     <property name="stock">gtk-zoom-out</property>
1223                                     <property name="icon_size">1</property>
1224                                   </widget>
1225                                 </child>
1226                               </widget>
1227                             </child>
1228                             <child>
1229                               <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
1230                                 <property name="visible">True</property>
1231                                 <property name="label" translatable="yes">_Normal size</property>
1232                                 <property name="use_underline">True</property>
1233                                 <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1234                                 <child internal-child="image">
1235                                   <widget class="GtkImage" id="image1062">
1236                                     <property name="visible">True</property>
1237                                     <property name="stock">gtk-zoom-100</property>
1238                                     <property name="icon_size">1</property>
1239                                   </widget>
1240                                 </child>
1241                               </widget>
1242                             </child>
1243                             <child>
1244                               <widget class="GtkSeparatorMenuItem" id="separator12">
1245                                 <property name="visible">True</property>
1246                               </widget>
1247                             </child>
1248                             <child>
1249                               <widget class="GtkCheckMenuItem" id="ppNotationMenuItem">
1250                                 <property name="visible">True</property>
1251                                 <property name="label" translatable="yes">Pretty print notation</property>
1252                                 <property name="use_underline">True</property>
1253                                 <property name="active">True</property>
1254                               </widget>
1255                             </child>
1256                             <child>
1257                               <widget class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
1258                                 <property name="visible">True</property>
1259                                 <property name="label" translatable="yes">Hide coercions</property>
1260                                 <property name="use_underline">True</property>
1261                                 <property name="active">True</property>
1262                               </widget>
1263                             </child>
1264                             <child>
1265                               <widget class="GtkSeparatorMenuItem" id="separator13">
1266                                 <property name="visible">True</property>
1267                               </widget>
1268                             </child>
1269                             <child>
1270                               <widget class="GtkMenuItem" id="showCoercionsGraphMenuItem">
1271                                 <property name="visible">True</property>
1272                                 <property name="tooltip" translatable="yes">Displays the graph of coercions</property>
1273                                 <property name="label" translatable="yes">Coercions Graph</property>
1274                                 <property name="use_underline">True</property>
1275                               </widget>
1276                             </child>
1277                             <child>
1278                               <widget class="GtkImageMenuItem" id="showAutoGuiMenuItem">
1279                                 <property name="visible">True</property>
1280                                 <property name="tooltip" translatable="yes">Displays a window helpful to drive automation</property>
1281                                 <property name="label" translatable="yes">Auto GUI</property>
1282                                 <property name="use_underline">True</property>
1283                                 <child internal-child="image">
1284                                   <widget class="GtkImage" id="menu-item-image19">
1285                                     <property name="stock">gtk-media-pause</property>
1286                                   </widget>
1287                                 </child>
1288                               </widget>
1289                             </child>
1290                             <child>
1291                               <widget class="GtkImageMenuItem" id="showTermGrammarMenuItem">
1292                                 <property name="visible">True</property>
1293                                 <property name="tooltip" translatable="yes">Displays the term grammar</property>
1294                                 <property name="label" translatable="yes">Show term's grammar</property>
1295                                 <property name="use_underline">True</property>
1296                               </widget>
1297                             </child>
1298                           </widget>
1299                         </child>
1300                       </widget>
1301                     </child>
1302                     <child>
1303                       <widget class="GtkMenuItem" id="debugMenu">
1304                         <property name="visible">True</property>
1305                         <property name="label" translatable="yes">_Debug</property>
1306                         <property name="use_underline">True</property>
1307                         <child>
1308                           <widget class="GtkMenu" id="debugMenu_menu">
1309                             <child>
1310                               <widget class="GtkSeparatorMenuItem" id="separator6">
1311                                 <property name="visible">True</property>
1312                               </widget>
1313                             </child>
1314                           </widget>
1315                         </child>
1316                       </widget>
1317                     </child>
1318                     <child>
1319                       <widget class="GtkMenuItem" id="helpMenu">
1320                         <property name="visible">True</property>
1321                         <property name="label" translatable="yes">_Help</property>
1322                         <property name="use_underline">True</property>
1323                         <child>
1324                           <widget class="GtkMenu" id="helpMenu_menu">
1325                             <child>
1326                               <widget class="GtkImageMenuItem" id="contentsMenuItem">
1327                                 <property name="visible">True</property>
1328                                 <property name="label" translatable="yes">_Contents</property>
1329                                 <property name="use_underline">True</property>
1330                                 <accelerator key="F1" modifiers="" signal="activate"/>
1331                                 <child internal-child="image">
1332                                   <widget class="GtkImage" id="image1063">
1333                                     <property name="visible">True</property>
1334                                     <property name="stock">gtk-help</property>
1335                                     <property name="icon_size">1</property>
1336                                   </widget>
1337                                 </child>
1338                               </widget>
1339                             </child>
1340                             <child>
1341                               <widget class="GtkImageMenuItem" id="showUnicodeTable">
1342                                 <property name="visible">True</property>
1343                                 <property name="tooltip" translatable="yes">Displays the Tex/Unicode table</property>
1344                                 <property name="label" translatable="yes">Show Tex/Unicode table</property>
1345                                 <property name="use_underline">True</property>
1346                               </widget>
1347                             </child>
1348                             <child>
1349                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
1350                                 <property name="visible">True</property>
1351                                 <property name="label" translatable="yes">_About</property>
1352                                 <property name="use_underline">True</property>
1353                                 <child internal-child="image">
1354                                   <widget class="GtkImage" id="image1064">
1355                                     <property name="visible">True</property>
1356                                     <property name="stock">gtk-about</property>
1357                                     <property name="icon_size">1</property>
1358                                   </widget>
1359                                 </child>
1360                               </widget>
1361                             </child>
1362                           </widget>
1363                         </child>
1364                       </widget>
1365                     </child>
1366                   </widget>
1367                 </child>
1368               </widget>
1369               <packing>
1370                 <property name="expand">False</property>
1371                 <property name="fill">False</property>
1372               </packing>
1373             </child>
1374             <child>
1375               <widget class="GtkHBox" id="hbox99">
1376                 <property name="visible">True</property>
1377                 <child>
1378                   <widget class="GtkHPaned" id="hpaneScriptSequent">
1379                     <property name="visible">True</property>
1380                     <property name="can_focus">True</property>
1381                     <child>
1382                       <widget class="GtkHBox" id="hbox18">
1383                         <property name="visible">True</property>
1384                         <child>
1385                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1386                             <property name="visible">True</property>
1387                             <property name="shadow_type">GTK_SHADOW_OUT</property>
1388                             <property name="handle_position">GTK_POS_TOP</property>
1389                             <child>
1390                               <widget class="GtkVBox" id="vboxTacticsPalette">
1391                                 <property name="visible">True</property>
1392                                 <child>
1393                                   <placeholder/>
1394                                 </child>
1395                                 <child>
1396                                   <placeholder/>
1397                                 </child>
1398                                 <child>
1399                                   <placeholder/>
1400                                 </child>
1401                               </widget>
1402                             </child>
1403                           </widget>
1404                           <packing>
1405                             <property name="expand">False</property>
1406                           </packing>
1407                         </child>
1408                         <child>
1409                           <widget class="GtkVBox" id="vboxScript">
1410                             <property name="width_request">400</property>
1411                             <property name="visible">True</property>
1412                             <child>
1413                               <widget class="GtkHBox" id="hbox28">
1414                                 <property name="visible">True</property>
1415                                 <child>
1416                                   <widget class="GtkToolbar" id="buttonsToolbar">
1417                                     <property name="visible">True</property>
1418                                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1419                                     <child>
1420                                       <widget class="GtkToolItem" id="toolitem41">
1421                                         <property name="visible">True</property>
1422                                         <child>
1423                                           <widget class="GtkButton" id="scriptTopButton">
1424                                             <property name="visible">True</property>
1425                                             <property name="can_focus">True</property>
1426                                             <property name="tooltip" translatable="yes">Restart</property>
1427                                             <property name="relief">GTK_RELIEF_NONE</property>
1428                                             <property name="response_id">0</property>
1429                                             <child>
1430                                               <widget class="GtkImage" id="image920">
1431                                                 <property name="visible">True</property>
1432                                                 <property name="stock">gtk-goto-top</property>
1433                                               </widget>
1434                                             </child>
1435                                           </widget>
1436                                         </child>
1437                                       </widget>
1438                                       <packing>
1439                                         <property name="expand">False</property>
1440                                         <property name="homogeneous">False</property>
1441                                       </packing>
1442                                     </child>
1443                                     <child>
1444                                       <widget class="GtkToolItem" id="toolitem42">
1445                                         <property name="visible">True</property>
1446                                         <child>
1447                                           <widget class="GtkButton" id="scriptRetractButton">
1448                                             <property name="visible">True</property>
1449                                             <property name="can_focus">True</property>
1450                                             <property name="tooltip" translatable="yes">Retract 1 phrase</property>
1451                                             <property name="relief">GTK_RELIEF_NONE</property>
1452                                             <property name="response_id">0</property>
1453                                             <child>
1454                                               <widget class="GtkImage" id="image921">
1455                                                 <property name="visible">True</property>
1456                                                 <property name="stock">gtk-go-up</property>
1457                                               </widget>
1458                                             </child>
1459                                           </widget>
1460                                         </child>
1461                                       </widget>
1462                                       <packing>
1463                                         <property name="expand">False</property>
1464                                         <property name="homogeneous">False</property>
1465                                       </packing>
1466                                     </child>
1467                                     <child>
1468                                       <widget class="GtkToolItem" id="toolitem43">
1469                                         <property name="visible">True</property>
1470                                         <child>
1471                                           <widget class="GtkButton" id="scriptJumpButton">
1472                                             <property name="visible">True</property>
1473                                             <property name="can_focus">True</property>
1474                                             <property name="tooltip" translatable="yes">Execute until point</property>
1475                                             <property name="relief">GTK_RELIEF_NONE</property>
1476                                             <property name="response_id">0</property>
1477                                             <child>
1478                                               <widget class="GtkImage" id="image922">
1479                                                 <property name="visible">True</property>
1480                                                 <property name="stock">gtk-jump-to</property>
1481                                               </widget>
1482                                             </child>
1483                                           </widget>
1484                                         </child>
1485                                       </widget>
1486                                       <packing>
1487                                         <property name="expand">False</property>
1488                                         <property name="homogeneous">False</property>
1489                                       </packing>
1490                                     </child>
1491                                     <child>
1492                                       <widget class="GtkToolItem" id="toolitem44">
1493                                         <property name="visible">True</property>
1494                                         <child>
1495                                           <widget class="GtkButton" id="scriptAdvanceButton">
1496                                             <property name="visible">True</property>
1497                                             <property name="can_focus">True</property>
1498                                             <property name="tooltip" translatable="yes">Execute 1 phrase</property>
1499                                             <property name="relief">GTK_RELIEF_NONE</property>
1500                                             <property name="response_id">0</property>
1501                                             <child>
1502                                               <widget class="GtkImage" id="image923">
1503                                                 <property name="visible">True</property>
1504                                                 <property name="stock">gtk-go-down</property>
1505                                               </widget>
1506                                             </child>
1507                                           </widget>
1508                                         </child>
1509                                       </widget>
1510                                       <packing>
1511                                         <property name="expand">False</property>
1512                                         <property name="homogeneous">False</property>
1513                                       </packing>
1514                                     </child>
1515                                     <child>
1516                                       <widget class="GtkToolItem" id="toolitem45">
1517                                         <property name="visible">True</property>
1518                                         <child>
1519                                           <widget class="GtkButton" id="scriptBottomButton">
1520                                             <property name="visible">True</property>
1521                                             <property name="can_focus">True</property>
1522                                             <property name="tooltip" translatable="yes">Execute all</property>
1523                                             <property name="relief">GTK_RELIEF_NONE</property>
1524                                             <property name="response_id">0</property>
1525                                             <child>
1526                                               <widget class="GtkImage" id="image924">
1527                                                 <property name="visible">True</property>
1528                                                 <property name="stock">gtk-goto-bottom</property>
1529                                               </widget>
1530                                             </child>
1531                                           </widget>
1532                                         </child>
1533                                       </widget>
1534                                       <packing>
1535                                         <property name="expand">False</property>
1536                                         <property name="homogeneous">False</property>
1537                                       </packing>
1538                                     </child>
1539                                   </widget>
1540                                 </child>
1541                                 <child>
1542                                   <widget class="GtkToolbar" id="toolbar2">
1543                                     <property name="visible">True</property>
1544                                     <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
1545                                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1546                                     <child>
1547                                       <widget class="GtkToolItem" id="toolitem46">
1548                                         <property name="visible">True</property>
1549                                         <child>
1550                                           <widget class="GtkButton" id="scriptAbortButton">
1551                                             <property name="visible">True</property>
1552                                             <property name="can_focus">True</property>
1553                                             <property name="relief">GTK_RELIEF_NONE</property>
1554                                             <property name="response_id">0</property>
1555                                             <child>
1556                                               <widget class="GtkImage" id="image927">
1557                                                 <property name="visible">True</property>
1558                                                 <property name="stock">gtk-stop</property>
1559                                               </widget>
1560                                             </child>
1561                                           </widget>
1562                                         </child>
1563                                       </widget>
1564                                       <packing>
1565                                         <property name="expand">False</property>
1566                                         <property name="homogeneous">False</property>
1567                                       </packing>
1568                                     </child>
1569                                   </widget>
1570                                   <packing>
1571                                     <property name="expand">False</property>
1572                                     <property name="position">1</property>
1573                                   </packing>
1574                                 </child>
1575                               </widget>
1576                               <packing>
1577                                 <property name="expand">False</property>
1578                                 <property name="fill">False</property>
1579                               </packing>
1580                             </child>
1581                             <child>
1582                               <widget class="GtkNotebook" id="scriptNotebook">
1583                                 <property name="visible">True</property>
1584                                 <property name="can_focus">True</property>
1585                                 <property name="tab_pos">GTK_POS_BOTTOM</property>
1586                                 <child>
1587                                   <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
1588                                     <property name="visible">True</property>
1589                                     <property name="can_focus">True</property>
1590                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1591                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1592                                     <child>
1593                                       <placeholder/>
1594                                     </child>
1595                                   </widget>
1596                                 </child>
1597                                 <child>
1598                                   <widget class="GtkLabel" id="scriptLabel">
1599                                     <property name="visible">True</property>
1600                                     <property name="label" translatable="yes">script</property>
1601                                   </widget>
1602                                   <packing>
1603                                     <property name="type">tab</property>
1604                                     <property name="tab_fill">False</property>
1605                                   </packing>
1606                                 </child>
1607                                 <child>
1608                                   <widget class="GtkScrolledWindow" id="scrolledwindow8">
1609                                     <property name="visible">True</property>
1610                                     <property name="can_focus">True</property>
1611                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1612                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1613                                     <child>
1614                                       <widget class="GtkViewport" id="viewport1">
1615                                         <property name="visible">True</property>
1616                                         <child>
1617                                           <widget class="GtkLabel" id="label25">
1618                                             <property name="visible">True</property>
1619                                             <property name="label" translatable="yes">Not implemented.</property>
1620                                           </widget>
1621                                         </child>
1622                                       </widget>
1623                                     </child>
1624                                   </widget>
1625                                   <packing>
1626                                     <property name="position">1</property>
1627                                   </packing>
1628                                 </child>
1629                                 <child>
1630                                   <widget class="GtkLabel" id="label13">
1631                                     <property name="visible">True</property>
1632                                     <property name="label" translatable="yes">outline</property>
1633                                   </widget>
1634                                   <packing>
1635                                     <property name="type">tab</property>
1636                                     <property name="position">1</property>
1637                                     <property name="tab_fill">False</property>
1638                                   </packing>
1639                                 </child>
1640                               </widget>
1641                               <packing>
1642                                 <property name="position">1</property>
1643                               </packing>
1644                             </child>
1645                           </widget>
1646                           <packing>
1647                             <property name="position">1</property>
1648                           </packing>
1649                         </child>
1650                       </widget>
1651                       <packing>
1652                         <property name="resize">False</property>
1653                         <property name="shrink">True</property>
1654                       </packing>
1655                     </child>
1656                     <child>
1657                       <widget class="GtkVPaned" id="vpaned1">
1658                         <property name="width_request">250</property>
1659                         <property name="height_request">500</property>
1660                         <property name="visible">True</property>
1661                         <property name="can_focus">True</property>
1662                         <property name="position">380</property>
1663                         <child>
1664                           <widget class="GtkNotebook" id="sequentsNotebook">
1665                             <property name="visible">True</property>
1666                             <property name="can_focus">True</property>
1667                           </widget>
1668                           <packing>
1669                             <property name="resize">False</property>
1670                             <property name="shrink">True</property>
1671                           </packing>
1672                         </child>
1673                         <child>
1674                           <widget class="GtkHBox" id="hbox9">
1675                             <property name="visible">True</property>
1676                             <child>
1677                               <widget class="GtkScrolledWindow" id="logScrolledWin">
1678                                 <property name="visible">True</property>
1679                                 <property name="can_focus">True</property>
1680                                 <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
1681                                 <property name="shadow_type">GTK_SHADOW_IN</property>
1682                                 <child>
1683                                   <widget class="GtkTextView" id="logTextView">
1684                                     <property name="visible">True</property>
1685                                     <property name="can_focus">True</property>
1686                                     <property name="editable">False</property>
1687                                     <property name="wrap_mode">GTK_WRAP_CHAR</property>
1688                                     <property name="cursor_visible">False</property>
1689                                   </widget>
1690                                 </child>
1691                               </widget>
1692                             </child>
1693                           </widget>
1694                           <packing>
1695                             <property name="resize">True</property>
1696                             <property name="shrink">True</property>
1697                           </packing>
1698                         </child>
1699                       </widget>
1700                       <packing>
1701                         <property name="resize">True</property>
1702                         <property name="shrink">True</property>
1703                       </packing>
1704                     </child>
1705                   </widget>
1706                 </child>
1707               </widget>
1708               <packing>
1709                 <property name="position">1</property>
1710               </packing>
1711             </child>
1712             <child>
1713               <widget class="GtkHBox" id="hbox10">
1714                 <property name="visible">True</property>
1715                 <child>
1716                   <widget class="GtkStatusbar" id="StatusBar">
1717                     <property name="visible">True</property>
1718                     <property name="has_resize_grip">False</property>
1719                   </widget>
1720                 </child>
1721                 <child>
1722                   <widget class="GtkNotebook" id="HintNotebook">
1723                     <property name="visible">True</property>
1724                     <property name="show_tabs">False</property>
1725                     <child>
1726                       <widget class="GtkImage" id="HintLowImage">
1727                         <property name="visible">True</property>
1728                         <property name="stock">gtk-missing-image</property>
1729                       </widget>
1730                     </child>
1731                     <child>
1732                       <widget class="GtkLabel" id="label14">
1733                         <property name="visible">True</property>
1734                         <property name="label" translatable="yes">label14</property>
1735                       </widget>
1736                       <packing>
1737                         <property name="type">tab</property>
1738                         <property name="tab_fill">False</property>
1739                       </packing>
1740                     </child>
1741                     <child>
1742                       <widget class="GtkImage" id="HintMediumImage">
1743                         <property name="visible">True</property>
1744                         <property name="stock">gtk-missing-image</property>
1745                       </widget>
1746                       <packing>
1747                         <property name="position">1</property>
1748                       </packing>
1749                     </child>
1750                     <child>
1751                       <widget class="GtkLabel" id="label15">
1752                         <property name="visible">True</property>
1753                         <property name="label" translatable="yes">label15</property>
1754                       </widget>
1755                       <packing>
1756                         <property name="type">tab</property>
1757                         <property name="position">1</property>
1758                         <property name="tab_fill">False</property>
1759                       </packing>
1760                     </child>
1761                     <child>
1762                       <widget class="GtkImage" id="HintHighImage">
1763                         <property name="visible">True</property>
1764                         <property name="stock">gtk-missing-image</property>
1765                       </widget>
1766                       <packing>
1767                         <property name="position">2</property>
1768                       </packing>
1769                     </child>
1770                     <child>
1771                       <widget class="GtkLabel" id="label16">
1772                         <property name="visible">True</property>
1773                         <property name="label" translatable="yes">label16</property>
1774                       </widget>
1775                       <packing>
1776                         <property name="type">tab</property>
1777                         <property name="position">2</property>
1778                         <property name="tab_fill">False</property>
1779                       </packing>
1780                     </child>
1781                   </widget>
1782                   <packing>
1783                     <property name="expand">False</property>
1784                     <property name="position">1</property>
1785                   </packing>
1786                 </child>
1787               </widget>
1788               <packing>
1789                 <property name="expand">False</property>
1790                 <property name="fill">False</property>
1791                 <property name="position">2</property>
1792               </packing>
1793             </child>
1794           </widget>
1795         </child>
1796       </widget>
1797     </child>
1798   </widget>
1799   <widget class="GtkDialog" id="TextDialog">
1800     <property name="title" translatable="yes">DUMMY</property>
1801     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1802     <child internal-child="vbox">
1803       <widget class="GtkVBox" id="vbox5">
1804         <property name="visible">True</property>
1805         <child>
1806           <widget class="GtkLabel" id="TextDialogLabel">
1807             <property name="visible">True</property>
1808             <property name="label" translatable="yes">DUMMY</property>
1809           </widget>
1810           <packing>
1811             <property name="expand">False</property>
1812             <property name="fill">False</property>
1813             <property name="position">2</property>
1814           </packing>
1815         </child>
1816         <child>
1817           <widget class="GtkScrolledWindow" id="scrolledwindow2">
1818             <property name="visible">True</property>
1819             <property name="can_focus">True</property>
1820             <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1821             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1822             <property name="shadow_type">GTK_SHADOW_IN</property>
1823             <child>
1824               <widget class="GtkTextView" id="TextDialogTextView">
1825                 <property name="visible">True</property>
1826                 <property name="can_focus">True</property>
1827               </widget>
1828             </child>
1829           </widget>
1830           <packing>
1831             <property name="position">3</property>
1832           </packing>
1833         </child>
1834         <child internal-child="action_area">
1835           <widget class="GtkHButtonBox" id="hbuttonbox1">
1836             <property name="visible">True</property>
1837             <property name="layout_style">GTK_BUTTONBOX_END</property>
1838             <child>
1839               <widget class="GtkButton" id="TextDialogCancelButton">
1840                 <property name="visible">True</property>
1841                 <property name="can_focus">True</property>
1842                 <property name="can_default">True</property>
1843                 <property name="label">gtk-cancel</property>
1844                 <property name="use_stock">True</property>
1845                 <property name="response_id">-6</property>
1846               </widget>
1847             </child>
1848             <child>
1849               <widget class="GtkButton" id="TextDialogOkButton">
1850                 <property name="visible">True</property>
1851                 <property name="can_focus">True</property>
1852                 <property name="can_default">True</property>
1853                 <property name="label">gtk-ok</property>
1854                 <property name="use_stock">True</property>
1855                 <property name="response_id">-5</property>
1856               </widget>
1857               <packing>
1858                 <property name="position">1</property>
1859               </packing>
1860             </child>
1861           </widget>
1862           <packing>
1863             <property name="expand">False</property>
1864             <property name="pack_type">GTK_PACK_END</property>
1865           </packing>
1866         </child>
1867       </widget>
1868     </child>
1869   </widget>
1870   <widget class="GtkDialog" id="UriChoiceDialog">
1871     <property name="height_request">280</property>
1872     <property name="title" translatable="yes">Uri choice</property>
1873     <property name="modal">True</property>
1874     <property name="window_position">GTK_WIN_POS_CENTER</property>
1875     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1876     <child internal-child="vbox">
1877       <widget class="GtkVBox" id="dialog-vbox3">
1878         <property name="visible">True</property>
1879         <property name="spacing">4</property>
1880         <child>
1881           <widget class="GtkVBox" id="vbox2">
1882             <property name="visible">True</property>
1883             <property name="spacing">3</property>
1884             <child>
1885               <widget class="GtkLabel" id="UriChoiceLabel">
1886                 <property name="visible">True</property>
1887                 <property name="label" translatable="yes">some informative message here ...</property>
1888               </widget>
1889               <packing>
1890                 <property name="expand">False</property>
1891                 <property name="fill">False</property>
1892               </packing>
1893             </child>
1894             <child>
1895               <widget class="GtkScrolledWindow" id="scrolledwindow1">
1896                 <property name="width_request">400</property>
1897                 <property name="visible">True</property>
1898                 <property name="can_focus">True</property>
1899                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1900                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1901                 <child>
1902                   <widget class="GtkTreeView" id="UriChoiceTreeView">
1903                     <property name="visible">True</property>
1904                     <property name="can_focus">True</property>
1905                     <property name="headers_visible">False</property>
1906                   </widget>
1907                 </child>
1908               </widget>
1909               <packing>
1910                 <property name="position">1</property>
1911               </packing>
1912             </child>
1913             <child>
1914               <widget class="GtkHBox" id="uriEntryHBox">
1915                 <property name="visible">True</property>
1916                 <child>
1917                   <widget class="GtkLabel" id="label2">
1918                     <property name="visible">True</property>
1919                     <property name="label" translatable="yes">URI: </property>
1920                   </widget>
1921                   <packing>
1922                     <property name="expand">False</property>
1923                     <property name="fill">False</property>
1924                   </packing>
1925                 </child>
1926                 <child>
1927                   <widget class="GtkEntry" id="entry1">
1928                     <property name="visible">True</property>
1929                     <property name="can_focus">True</property>
1930                     <property name="invisible_char">*</property>
1931                   </widget>
1932                   <packing>
1933                     <property name="position">1</property>
1934                   </packing>
1935                 </child>
1936               </widget>
1937               <packing>
1938                 <property name="expand">False</property>
1939                 <property name="position">2</property>
1940               </packing>
1941             </child>
1942           </widget>
1943           <packing>
1944             <property name="position">2</property>
1945           </packing>
1946         </child>
1947         <child internal-child="action_area">
1948           <widget class="GtkHButtonBox" id="dialog-action_area3">
1949             <property name="visible">True</property>
1950             <property name="layout_style">GTK_BUTTONBOX_END</property>
1951             <child>
1952               <widget class="GtkButton" id="UriChoiceAbortButton">
1953                 <property name="visible">True</property>
1954                 <property name="can_focus">True</property>
1955                 <property name="can_default">True</property>
1956                 <property name="label">gtk-cancel</property>
1957                 <property name="use_stock">True</property>
1958                 <property name="response_id">-6</property>
1959               </widget>
1960             </child>
1961             <child>
1962               <widget class="GtkButton" id="UriChoiceSelectedButton">
1963                 <property name="visible">True</property>
1964                 <property name="can_focus">True</property>
1965                 <property name="can_default">True</property>
1966                 <property name="response_id">0</property>
1967                 <child>
1968                   <widget class="GtkAlignment" id="alignment2">
1969                     <property name="visible">True</property>
1970                     <property name="xscale">0</property>
1971                     <property name="yscale">0</property>
1972                     <child>
1973                       <widget class="GtkHBox" id="hbox3">
1974                         <property name="visible">True</property>
1975                         <property name="spacing">2</property>
1976                         <child>
1977                           <widget class="GtkImage" id="image19">
1978                             <property name="visible">True</property>
1979                             <property name="stock">gtk-index</property>
1980                           </widget>
1981                           <packing>
1982                             <property name="expand">False</property>
1983                             <property name="fill">False</property>
1984                           </packing>
1985                         </child>
1986                         <child>
1987                           <widget class="GtkLabel" id="label3">
1988                             <property name="visible">True</property>
1989                             <property name="label" translatable="yes">Try _Selected</property>
1990                             <property name="use_underline">True</property>
1991                           </widget>
1992                           <packing>
1993                             <property name="expand">False</property>
1994                             <property name="fill">False</property>
1995                             <property name="position">1</property>
1996                           </packing>
1997                         </child>
1998                       </widget>
1999                     </child>
2000                   </widget>
2001                 </child>
2002               </widget>
2003               <packing>
2004                 <property name="position">1</property>
2005               </packing>
2006             </child>
2007             <child>
2008               <widget class="GtkButton" id="UriChoiceConstantsButton">
2009                 <property name="visible">True</property>
2010                 <property name="sensitive">False</property>
2011                 <property name="can_focus">True</property>
2012                 <property name="can_default">True</property>
2013                 <property name="label" translatable="yes">Try Constants</property>
2014                 <property name="use_underline">True</property>
2015                 <property name="response_id">0</property>
2016               </widget>
2017               <packing>
2018                 <property name="position">2</property>
2019               </packing>
2020             </child>
2021             <child>
2022               <widget class="GtkButton" id="copyButton">
2023                 <property name="can_focus">True</property>
2024                 <property name="can_default">True</property>
2025                 <property name="label">gtk-copy</property>
2026                 <property name="use_stock">True</property>
2027                 <property name="response_id">0</property>
2028               </widget>
2029               <packing>
2030                 <property name="position">3</property>
2031               </packing>
2032             </child>
2033             <child>
2034               <widget class="GtkButton" id="uriChoiceAutoButton">
2035                 <property name="visible">True</property>
2036                 <property name="can_focus">True</property>
2037                 <property name="can_default">True</property>
2038                 <property name="response_id">0</property>
2039                 <child>
2040                   <widget class="GtkAlignment" id="alignment5">
2041                     <property name="visible">True</property>
2042                     <property name="xscale">0</property>
2043                     <property name="yscale">0</property>
2044                     <child>
2045                       <widget class="GtkHBox" id="hbox16">
2046                         <property name="visible">True</property>
2047                         <property name="spacing">2</property>
2048                         <child>
2049                           <widget class="GtkImage" id="image302">
2050                             <property name="visible">True</property>
2051                             <property name="stock">gtk-ok</property>
2052                           </widget>
2053                           <packing>
2054                             <property name="expand">False</property>
2055                             <property name="fill">False</property>
2056                           </packing>
2057                         </child>
2058                         <child>
2059                           <widget class="GtkLabel" id="okLabel">
2060                             <property name="visible">True</property>
2061                             <property name="label" translatable="yes">bla bla bla</property>
2062                             <property name="use_underline">True</property>
2063                           </widget>
2064                           <packing>
2065                             <property name="expand">False</property>
2066                             <property name="fill">False</property>
2067                             <property name="position">1</property>
2068                           </packing>
2069                         </child>
2070                       </widget>
2071                     </child>
2072                   </widget>
2073                 </child>
2074               </widget>
2075               <packing>
2076                 <property name="position">4</property>
2077               </packing>
2078             </child>
2079             <child>
2080               <widget class="GtkButton" id="uriChoiceForwardButton">
2081                 <property name="visible">True</property>
2082                 <property name="can_focus">True</property>
2083                 <property name="can_default">True</property>
2084                 <property name="label">gtk-go-forward</property>
2085                 <property name="use_stock">True</property>
2086                 <property name="response_id">0</property>
2087               </widget>
2088               <packing>
2089                 <property name="position">5</property>
2090               </packing>
2091             </child>
2092           </widget>
2093           <packing>
2094             <property name="expand">False</property>
2095             <property name="pack_type">GTK_PACK_END</property>
2096           </packing>
2097         </child>
2098       </widget>
2099     </child>
2100   </widget>
2101   <widget class="GtkWindow" id="FindReplWin">
2102     <property name="border_width">5</property>
2103     <property name="title" translatable="yes">Find &amp; Replace</property>
2104     <property name="resizable">False</property>
2105     <property name="window_position">GTK_WIN_POS_MOUSE</property>
2106     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2107     <child>
2108       <widget class="GtkTable" id="table1">
2109         <property name="visible">True</property>
2110         <property name="n_rows">3</property>
2111         <property name="n_columns">2</property>
2112         <property name="row_spacing">5</property>
2113         <child>
2114           <widget class="GtkHBox" id="hbox19">
2115             <property name="visible">True</property>
2116             <property name="spacing">5</property>
2117             <child>
2118               <widget class="GtkVBox" id="vbox9">
2119                 <property name="visible">True</property>
2120                 <child>
2121                   <placeholder/>
2122                 </child>
2123                 <child>
2124                   <placeholder/>
2125                 </child>
2126               </widget>
2127             </child>
2128             <child>
2129               <widget class="GtkButton" id="findButton">
2130                 <property name="visible">True</property>
2131                 <property name="can_focus">True</property>
2132                 <property name="label">gtk-find</property>
2133                 <property name="use_stock">True</property>
2134                 <property name="response_id">0</property>
2135               </widget>
2136               <packing>
2137                 <property name="expand">False</property>
2138                 <property name="fill">False</property>
2139                 <property name="position">1</property>
2140               </packing>
2141             </child>
2142             <child>
2143               <widget class="GtkButton" id="findReplButton">
2144                 <property name="visible">True</property>
2145                 <property name="can_focus">True</property>
2146                 <property name="response_id">0</property>
2147                 <child>
2148                   <widget class="GtkAlignment" id="alignment13">
2149                     <property name="visible">True</property>
2150                     <property name="xscale">0</property>
2151                     <property name="yscale">0</property>
2152                     <child>
2153                       <widget class="GtkHBox" id="hbox20">
2154                         <property name="visible">True</property>
2155                         <property name="spacing">2</property>
2156                         <child>
2157                           <widget class="GtkImage" id="image357">
2158                             <property name="visible">True</property>
2159                             <property name="stock">gtk-find-and-replace</property>
2160                           </widget>
2161                           <packing>
2162                             <property name="expand">False</property>
2163                             <property name="fill">False</property>
2164                           </packing>
2165                         </child>
2166                         <child>
2167                           <widget class="GtkLabel" id="label19">
2168                             <property name="visible">True</property>
2169                             <property name="label">_Replace</property>
2170                             <property name="use_underline">True</property>
2171                           </widget>
2172                           <packing>
2173                             <property name="expand">False</property>
2174                             <property name="fill">False</property>
2175                             <property name="position">1</property>
2176                           </packing>
2177                         </child>
2178                       </widget>
2179                     </child>
2180                   </widget>
2181                 </child>
2182               </widget>
2183               <packing>
2184                 <property name="expand">False</property>
2185                 <property name="fill">False</property>
2186                 <property name="position">2</property>
2187               </packing>
2188             </child>
2189             <child>
2190               <widget class="GtkButton" id="cancelButton">
2191                 <property name="visible">True</property>
2192                 <property name="can_focus">True</property>
2193                 <property name="label">gtk-cancel</property>
2194                 <property name="use_stock">True</property>
2195                 <property name="response_id">0</property>
2196               </widget>
2197               <packing>
2198                 <property name="expand">False</property>
2199                 <property name="fill">False</property>
2200                 <property name="position">3</property>
2201               </packing>
2202             </child>
2203           </widget>
2204           <packing>
2205             <property name="right_attach">2</property>
2206             <property name="top_attach">2</property>
2207             <property name="bottom_attach">3</property>
2208             <property name="y_padding">5</property>
2209           </packing>
2210         </child>
2211         <child>
2212           <widget class="GtkEntry" id="replaceEntry">
2213             <property name="visible">True</property>
2214             <property name="can_focus">True</property>
2215             <property name="invisible_char">*</property>
2216           </widget>
2217           <packing>
2218             <property name="left_attach">1</property>
2219             <property name="right_attach">2</property>
2220             <property name="top_attach">1</property>
2221             <property name="bottom_attach">2</property>
2222             <property name="y_options"></property>
2223           </packing>
2224         </child>
2225         <child>
2226           <widget class="GtkEntry" id="findEntry">
2227             <property name="visible">True</property>
2228             <property name="can_focus">True</property>
2229             <property name="has_focus">True</property>
2230             <property name="can_default">True</property>
2231             <property name="has_default">True</property>
2232             <property name="invisible_char">*</property>
2233           </widget>
2234           <packing>
2235             <property name="left_attach">1</property>
2236             <property name="right_attach">2</property>
2237             <property name="y_options"></property>
2238           </packing>
2239         </child>
2240         <child>
2241           <widget class="GtkLabel" id="label18">
2242             <property name="visible">True</property>
2243             <property name="xalign">0</property>
2244             <property name="label" translatable="yes">Replace with: </property>
2245           </widget>
2246           <packing>
2247             <property name="top_attach">1</property>
2248             <property name="bottom_attach">2</property>
2249             <property name="x_options"></property>
2250             <property name="y_options"></property>
2251           </packing>
2252         </child>
2253         <child>
2254           <widget class="GtkLabel" id="label17">
2255             <property name="visible">True</property>
2256             <property name="xalign">0</property>
2257             <property name="label" translatable="yes">Find:</property>
2258           </widget>
2259           <packing>
2260             <property name="x_options"></property>
2261             <property name="y_options"></property>
2262           </packing>
2263         </child>
2264       </widget>
2265     </child>
2266   </widget>
2267   <widget class="GtkDialog" id="DisambiguationErrors">
2268     <property name="width_request">450</property>
2269     <property name="height_request">400</property>
2270     <property name="title" translatable="yes">title</property>
2271     <property name="modal">True</property>
2272     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2273     <child internal-child="vbox">
2274       <widget class="GtkVBox" id="vbox14">
2275         <property name="visible">True</property>
2276         <child>
2277           <widget class="GtkVBox" id="vbox15">
2278             <property name="visible">True</property>
2279             <child>
2280               <widget class="GtkLabel" id="disambiguationErrorsLabel">
2281                 <property name="visible">True</property>
2282                 <property name="label" translatable="yes">some informative message here ...</property>
2283               </widget>
2284               <packing>
2285                 <property name="expand">False</property>
2286                 <property name="fill">False</property>
2287               </packing>
2288             </child>
2289             <child>
2290               <widget class="GtkScrolledWindow" id="scrolledwindow12">
2291                 <property name="visible">True</property>
2292                 <property name="can_focus">True</property>
2293                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2294                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2295                 <property name="shadow_type">GTK_SHADOW_IN</property>
2296                 <child>
2297                   <widget class="GtkTreeView" id="treeview">
2298                     <property name="visible">True</property>
2299                     <property name="can_focus">True</property>
2300                     <property name="headers_visible">False</property>
2301                   </widget>
2302                 </child>
2303               </widget>
2304               <packing>
2305                 <property name="position">1</property>
2306               </packing>
2307             </child>
2308           </widget>
2309           <packing>
2310             <property name="position">2</property>
2311           </packing>
2312         </child>
2313         <child internal-child="action_area">
2314           <widget class="GtkHButtonBox" id="hbuttonbox2">
2315             <property name="visible">True</property>
2316             <property name="layout_style">GTK_BUTTONBOX_END</property>
2317             <child>
2318               <widget class="GtkButton" id="button6">
2319                 <property name="visible">True</property>
2320                 <property name="can_focus">True</property>
2321                 <property name="can_default">True</property>
2322                 <property name="label">gtk-help</property>
2323                 <property name="use_stock">True</property>
2324                 <property name="response_id">-11</property>
2325               </widget>
2326             </child>
2327             <child>
2328               <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
2329                 <property name="visible">True</property>
2330                 <property name="can_focus">True</property>
2331                 <property name="can_default">True</property>
2332                 <property name="response_id">-6</property>
2333                 <child>
2334                   <widget class="GtkAlignment" id="alignment18">
2335                     <property name="visible">True</property>
2336                     <property name="xscale">0</property>
2337                     <property name="yscale">0</property>
2338                     <child>
2339                       <widget class="GtkHBox" id="hbox29">
2340                         <property name="visible">True</property>
2341                         <property name="spacing">2</property>
2342                         <child>
2343                           <widget class="GtkImage" id="image926">
2344                             <property name="visible">True</property>
2345                             <property name="stock">gtk-zoom-in</property>
2346                           </widget>
2347                           <packing>
2348                             <property name="expand">False</property>
2349                             <property name="fill">False</property>
2350                           </packing>
2351                         </child>
2352                         <child>
2353                           <widget class="GtkLabel" id="label28">
2354                             <property name="visible">True</property>
2355                             <property name="label">More</property>
2356                             <property name="use_underline">True</property>
2357                           </widget>
2358                           <packing>
2359                             <property name="expand">False</property>
2360                             <property name="fill">False</property>
2361                             <property name="position">1</property>
2362                           </packing>
2363                         </child>
2364                       </widget>
2365                     </child>
2366                   </widget>
2367                 </child>
2368               </widget>
2369               <packing>
2370                 <property name="position">1</property>
2371               </packing>
2372             </child>
2373             <child>
2374               <widget class="GtkButton" id="disambiguationErrorsCancelButton">
2375                 <property name="visible">True</property>
2376                 <property name="can_focus">True</property>
2377                 <property name="can_default">True</property>
2378                 <property name="has_default">True</property>
2379                 <property name="label">gtk-cancel</property>
2380                 <property name="use_stock">True</property>
2381                 <property name="response_id">-6</property>
2382               </widget>
2383               <packing>
2384                 <property name="position">2</property>
2385               </packing>
2386             </child>
2387             <child>
2388               <widget class="GtkButton" id="disambiguationErrorsOkButton">
2389                 <property name="visible">True</property>
2390                 <property name="can_focus">True</property>
2391                 <property name="can_default">True</property>
2392                 <property name="label">gtk-ok</property>
2393                 <property name="use_stock">True</property>
2394                 <property name="response_id">-5</property>
2395               </widget>
2396               <packing>
2397                 <property name="position">3</property>
2398               </packing>
2399             </child>
2400           </widget>
2401           <packing>
2402             <property name="expand">False</property>
2403             <property name="pack_type">GTK_PACK_END</property>
2404           </packing>
2405         </child>
2406       </widget>
2407     </child>
2408   </widget>
2409   <widget class="GtkWindow" id="AutoWin">
2410     <property name="width_request">600</property>
2411     <property name="height_request">400</property>
2412     <property name="visible">True</property>
2413     <property name="title" translatable="yes">Auto</property>
2414     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2415     <property name="gravity">GDK_GRAVITY_SOUTH_EAST</property>
2416     <child>
2417       <widget class="GtkVBox" id="vbox17">
2418         <property name="visible">True</property>
2419         <child>
2420           <widget class="GtkHBox" id="hbox30">
2421             <property name="visible">True</property>
2422             <property name="spacing">2</property>
2423             <child>
2424               <widget class="GtkScrolledWindow" id="scrolledwindowAREA">
2425                 <property name="visible">True</property>
2426                 <property name="can_focus">True</property>
2427                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2428                 <property name="shadow_type">GTK_SHADOW_IN</property>
2429                 <child>
2430                   <widget class="GtkViewport" id="viewportAREA">
2431                     <property name="visible">True</property>
2432                     <child>
2433                       <widget class="GtkTable" id="table">
2434                         <property name="visible">True</property>
2435                         <property name="n_rows">3</property>
2436                         <property name="n_columns">3</property>
2437                         <child>
2438                           <placeholder/>
2439                         </child>
2440                         <child>
2441                           <placeholder/>
2442                         </child>
2443                         <child>
2444                           <placeholder/>
2445                         </child>
2446                         <child>
2447                           <placeholder/>
2448                         </child>
2449                         <child>
2450                           <placeholder/>
2451                         </child>
2452                         <child>
2453                           <placeholder/>
2454                         </child>
2455                         <child>
2456                           <placeholder/>
2457                         </child>
2458                         <child>
2459                           <placeholder/>
2460                         </child>
2461                         <child>
2462                           <placeholder/>
2463                         </child>
2464                       </widget>
2465                     </child>
2466                   </widget>
2467                 </child>
2468               </widget>
2469             </child>
2470             <child>
2471               <widget class="GtkVBox" id="vbox18">
2472                 <property name="visible">True</property>
2473                 <child>
2474                   <widget class="GtkButton" id="buttonUP">
2475                     <property name="visible">True</property>
2476                     <property name="can_focus">True</property>
2477                     <property name="response_id">0</property>
2478                     <child>
2479                       <widget class="GtkAlignment" id="alignment19">
2480                         <property name="visible">True</property>
2481                         <property name="xscale">0</property>
2482                         <property name="yscale">0</property>
2483                         <child>
2484                           <widget class="GtkHBox" id="hbox31">
2485                             <property name="visible">True</property>
2486                             <property name="spacing">2</property>
2487                             <child>
2488                               <widget class="GtkImage" id="image1066">
2489                                 <property name="visible">True</property>
2490                                 <property name="stock">gtk-go-up</property>
2491                               </widget>
2492                               <packing>
2493                                 <property name="expand">False</property>
2494                                 <property name="fill">False</property>
2495                               </packing>
2496                             </child>
2497                             <child>
2498                               <widget class="GtkLabel" id="label30">
2499                                 <property name="visible">True</property>
2500                                 <property name="use_underline">True</property>
2501                               </widget>
2502                               <packing>
2503                                 <property name="expand">False</property>
2504                                 <property name="fill">False</property>
2505                                 <property name="position">1</property>
2506                               </packing>
2507                             </child>
2508                           </widget>
2509                         </child>
2510                       </widget>
2511                     </child>
2512                   </widget>
2513                 </child>
2514                 <child>
2515                   <widget class="GtkButton" id="buttonDOWN">
2516                     <property name="visible">True</property>
2517                     <property name="can_focus">True</property>
2518                     <property name="response_id">0</property>
2519                     <child>
2520                       <widget class="GtkImage" id="image1065">
2521                         <property name="visible">True</property>
2522                         <property name="stock">gtk-go-down</property>
2523                       </widget>
2524                     </child>
2525                   </widget>
2526                   <packing>
2527                     <property name="position">1</property>
2528                   </packing>
2529                 </child>
2530               </widget>
2531               <packing>
2532                 <property name="expand">False</property>
2533                 <property name="fill">False</property>
2534                 <property name="position">1</property>
2535               </packing>
2536             </child>
2537           </widget>
2538         </child>
2539         <child>
2540           <widget class="GtkHSeparator" id="hseparator3">
2541             <property name="visible">True</property>
2542           </widget>
2543           <packing>
2544             <property name="expand">False</property>
2545             <property name="padding">3</property>
2546             <property name="position">1</property>
2547           </packing>
2548         </child>
2549         <child>
2550           <widget class="GtkHBox" id="hbox32">
2551             <property name="visible">True</property>
2552             <child>
2553               <widget class="GtkLabel" id="labelLAST">
2554                 <property name="visible">True</property>
2555                 <property name="xalign">0</property>
2556                 <property name="label" translatable="yes">Last:</property>
2557               </widget>
2558             </child>
2559             <child>
2560               <widget class="GtkHButtonBox" id="hbuttonbox3">
2561                 <property name="visible">True</property>
2562                 <property name="border_width">4</property>
2563                 <property name="spacing">4</property>
2564                 <property name="layout_style">GTK_BUTTONBOX_END</property>
2565                 <child>
2566                   <widget class="GtkButton" id="buttonPAUSE">
2567                     <property name="visible">True</property>
2568                     <property name="can_focus">True</property>
2569                     <property name="can_default">True</property>
2570                     <property name="label">gtk-media-pause</property>
2571                     <property name="use_stock">True</property>
2572                     <property name="response_id">0</property>
2573                   </widget>
2574                 </child>
2575                 <child>
2576                   <widget class="GtkButton" id="buttonPLAY">
2577                     <property name="visible">True</property>
2578                     <property name="can_focus">True</property>
2579                     <property name="can_default">True</property>
2580                     <property name="label">gtk-media-play</property>
2581                     <property name="use_stock">True</property>
2582                     <property name="response_id">0</property>
2583                   </widget>
2584                   <packing>
2585                     <property name="position">1</property>
2586                   </packing>
2587                 </child>
2588                 <child>
2589                   <widget class="GtkButton" id="buttonNEXT">
2590                     <property name="visible">True</property>
2591                     <property name="can_focus">True</property>
2592                     <property name="can_default">True</property>
2593                     <property name="label">gtk-media-next</property>
2594                     <property name="use_stock">True</property>
2595                     <property name="response_id">0</property>
2596                   </widget>
2597                   <packing>
2598                     <property name="position">2</property>
2599                   </packing>
2600                 </child>
2601                 <child>
2602                   <widget class="GtkButton" id="buttonCLOSE">
2603                     <property name="visible">True</property>
2604                     <property name="can_focus">True</property>
2605                     <property name="can_default">True</property>
2606                     <property name="label">gtk-close</property>
2607                     <property name="use_stock">True</property>
2608                     <property name="response_id">0</property>
2609                   </widget>
2610                   <packing>
2611                     <property name="position">3</property>
2612                   </packing>
2613                 </child>
2614               </widget>
2615               <packing>
2616                 <property name="position">1</property>
2617               </packing>
2618             </child>
2619           </widget>
2620           <packing>
2621             <property name="expand">False</property>
2622             <property name="position">2</property>
2623           </packing>
2624         </child>
2625       </widget>
2626     </child>
2627   </widget>
2628 </glade-interface>