]> matita.cs.unibo.it Git - helm.git/commitdiff
added comments, fixed history, added loadList to browser
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 May 2005 15:23:07 +0000 (15:23 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 May 2005 15:23:07 +0000 (15:23 +0000)
18 files changed:
helm/matita/matita.conf.xml
helm/matita/matita.glade
helm/matita/matita.ml
helm/matita/matita.txt
helm/matita/matitaEngine.ml
helm/matita/matitaGtkMisc.ml
helm/matita/matitaGtkMisc.mli
helm/matita/matitaGui.ml
helm/matita/matitaGui.mli
helm/matita/matitaMathView.ml
helm/matita/matitaMathView.mli
helm/matita/matitaMisc.ml
helm/matita/matitaMisc.mli
helm/matita/matitaScript.ml
helm/matita/matitaScript.mli
helm/matita/matitaTypes.ml
helm/matita/tests/test4.ma
helm/matita/tests/test_instance.ma

index 54f608692f9c983be6673000fd285917e8a1e343..07887c6bd42adfc351a4c1ca1ce16c52fb0e524a 100644 (file)
@@ -8,10 +8,10 @@
     <key name="owner">gares</key>
   </section>
   <section name="db">
-    <key name="host">localhost</key>
-    <!--    <key name="host">mowgli.cs.unibo.it</key> --> 
+    <!-- <key name="host">localhost</key> -->
+    <key name="host">mowgli.cs.unibo.it</key>
     <key name="user">helm</key>
-    <key name="database">mowgli</key>
+    <key name="database">matita</key>
   </section>
   <section name="getter">
     <key name="prefetch">true</key>
index 2704d164d3b49f0ffe61d8bfa5a86886f84de5ef..57ce4006ade69392ff95e4dadc0c8ab7f4fc0dbc 100644 (file)
@@ -79,13 +79,13 @@ Copyright (C) 2005,
 </widget>
 
 <widget class="GtkWindow" id="BrowserWin">
-  <property name="width_request">500</property>
-  <property name="height_request">500</property>
   <property name="visible">True</property>
   <property name="title" translatable="yes">Cic browser</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
-  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
   <property name="modal">False</property>
+  <property name="default_width">500</property>
+  <property name="default_height">500</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
   <property name="decorated">True</property>
@@ -107,26 +107,29 @@ Copyright (C) 2005,
          <property name="spacing">0</property>
 
          <child>
-           <widget class="GtkHandleBox" id="handlebox1">
+           <widget class="GtkFrame" id="frame2">
              <property name="visible">True</property>
+             <property name="label_xalign">0</property>
+             <property name="label_yalign">0.5</property>
              <property name="shadow_type">GTK_SHADOW_OUT</property>
-             <property name="handle_position">GTK_POS_LEFT</property>
-             <property name="snap_edge">GTK_POS_TOP</property>
 
              <child>
-               <widget class="GtkToolbar" id="toolbar14">
+               <widget class="GtkAlignment" id="alignment3">
                  <property name="visible">True</property>
-                 <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                 <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                 <property name="tooltips">True</property>
-                 <property name="show_arrow">True</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xscale">1</property>
+                 <property name="yscale">1</property>
+                 <property name="top_padding">0</property>
+                 <property name="bottom_padding">0</property>
+                 <property name="left_padding">0</property>
+                 <property name="right_padding">0</property>
 
                  <child>
-                   <widget class="GtkToolItem" id="toolitem30">
+                   <widget class="GtkHBox" id="hbox11">
                      <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
+                     <property name="homogeneous">False</property>
+                     <property name="spacing">0</property>
 
                      <child>
                        <widget class="GtkButton" id="BrowserNewButton">
@@ -135,7 +138,7 @@ Copyright (C) 2005,
                          <property name="can_default">True</property>
                          <property name="can_focus">True</property>
                          <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
+                         <property name="focus_on_click">False</property>
 
                          <child>
                            <widget class="GtkImage" id="image191">
@@ -149,20 +152,12 @@ Copyright (C) 2005,
                            </widget>
                          </child>
                        </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem31">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
                        <widget class="GtkButton" id="BrowserBackButton">
@@ -233,20 +228,12 @@ Copyright (C) 2005,
                            </widget>
                          </child>
                        </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem32">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
                        <widget class="GtkButton" id="BrowserForwardButton">
@@ -269,20 +256,12 @@ Copyright (C) 2005,
                            </widget>
                          </child>
                        </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem33">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
                        <widget class="GtkButton" id="BrowserRefreshButton">
@@ -305,20 +284,12 @@ Copyright (C) 2005,
                            </widget>
                          </child>
                        </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem34">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
                        <widget class="GtkButton" id="BrowserHomeButton">
@@ -341,23 +312,15 @@ Copyright (C) 2005,
                            </widget>
                          </child>
                        </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem35">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
-                       <widget class="GtkImage" id="image187">
+                       <widget class="GtkImage" id="image301">
                          <property name="visible">True</property>
                          <property name="stock">gtk-jump-to</property>
                          <property name="icon_size">4</property>
@@ -366,26 +329,20 @@ Copyright (C) 2005,
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
                        </widget>
+                       <packing>
+                         <property name="padding">3</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
-                   </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
-                 </child>
-
-                 <child>
-                   <widget class="GtkToolItem" id="toolitem36">
-                     <property name="visible">True</property>
-                     <property name="visible_horizontal">True</property>
-                     <property name="visible_vertical">True</property>
-                     <property name="is_important">False</property>
 
                      <child>
                        <widget class="GtkEntry" id="BrowserUri">
                          <property name="visible">True</property>
                          <property name="tooltip" translatable="yes">cic uri</property>
+                         <property name="can_default">True</property>
                          <property name="can_focus">True</property>
+                         <property name="has_focus">True</property>
                          <property name="editable">True</property>
                          <property name="visibility">True</property>
                          <property name="max_length">0</property>
@@ -393,14 +350,92 @@ Copyright (C) 2005,
                          <property name="has_frame">True</property>
                          <property name="invisible_char">*</property>
                          <property name="activates_default">False</property>
-                         <property name="width_chars">34</property>
                        </widget>
+                       <packing>
+                         <property name="padding">3</property>
+                         <property name="expand">True</property>
+                         <property name="fill">True</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkVBox" id="vbox14">
+                         <property name="width_request">20</property>
+                         <property name="visible">True</property>
+                         <property name="homogeneous">False</property>
+                         <property name="spacing">0</property>
+
+                         <child>
+                           <placeholder/>
+                         </child>
+
+                         <child>
+                           <placeholder/>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">True</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkImage" id="whelpImage2">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkToggleButton" id="whelpBarToggleButton">
+                         <property name="visible">True</property>
+                         <property name="can_focus">True</property>
+                         <property name="relief">GTK_RELIEF_NONE</property>
+                         <property name="focus_on_click">True</property>
+                         <property name="active">False</property>
+                         <property name="inconsistent">False</property>
+
+                         <child>
+                           <widget class="GtkHBox" id="hbox15">
+                             <property name="visible">True</property>
+                             <property name="homogeneous">False</property>
+                             <property name="spacing">0</property>
+
+                             <child>
+                               <widget class="GtkArrow" id="arrow1">
+                                 <property name="visible">True</property>
+                                 <property name="arrow_type">GTK_ARROW_DOWN</property>
+                                 <property name="shadow_type">GTK_SHADOW_NONE</property>
+                                 <property name="xalign">0.5</property>
+                                 <property name="yalign">0.5</property>
+                                 <property name="xpad">0</property>
+                                 <property name="ypad">0</property>
+                               </widget>
+                               <packing>
+                                 <property name="padding">0</property>
+                                 <property name="expand">True</property>
+                                 <property name="fill">True</property>
+                               </packing>
+                             </child>
+                           </widget>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
                      </child>
                    </widget>
-                   <packing>
-                     <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
-                   </packing>
                  </child>
                </widget>
              </child>
@@ -413,83 +448,232 @@ Copyright (C) 2005,
          </child>
 
          <child>
-           <widget class="GtkFrame" id="frame1">
+           <widget class="GtkHBox" id="whelpBarBox">
+             <property name="border_width">3</property>
              <property name="visible">True</property>
-             <property name="label_xalign">0</property>
-             <property name="label_yalign">0</property>
-             <property name="shadow_type">GTK_SHADOW_IN</property>
+             <property name="homogeneous">False</property>
+             <property name="spacing">6</property>
 
              <child>
-               <widget class="GtkScrolledWindow" id="ScrolledBrowser">
+               <widget class="GtkEntry" id="queryInputText">
                  <property name="visible">True</property>
                  <property name="can_focus">True</property>
-                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                 <property name="shadow_type">GTK_SHADOW_NONE</property>
-                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+                 <property name="editable">True</property>
+                 <property name="visibility">True</property>
+                 <property name="max_length">0</property>
+                 <property name="text" translatable="yes"></property>
+                 <property name="has_frame">True</property>
+                 <property name="invisible_char">*</property>
+                 <property name="activates_default">False</property>
+               </widget>
+               <packing>
+                 <property name="padding">0</property>
+                 <property name="expand">True</property>
+                 <property name="fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkVBox" id="comboVbox">
+                 <property name="visible">True</property>
+                 <property name="homogeneous">False</property>
+                 <property name="spacing">0</property>
 
                  <child>
-                   <placeholder/>
+                   <widget class="GtkAlignment" id="alignment4">
+                     <property name="visible">True</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xscale">1</property>
+                     <property name="yscale">1</property>
+                     <property name="top_padding">0</property>
+                     <property name="bottom_padding">0</property>
+                     <property name="left_padding">0</property>
+                     <property name="right_padding">0</property>
+
+                     <child>
+                       <placeholder/>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
                  </child>
                </widget>
+               <packing>
+                 <property name="padding">0</property>
+                 <property name="expand">False</property>
+                 <property name="fill">True</property>
+               </packing>
              </child>
            </widget>
            <packing>
              <property name="padding">0</property>
-             <property name="expand">True</property>
+             <property name="expand">False</property>
              <property name="fill">True</property>
            </packing>
          </child>
-       </widget>
-      </child>
-    </widget>
-  </child>
-</widget>
-
-<widget class="GtkDialog" id="ConfirmationDialog">
-  <property name="title" translatable="yes">DUMMY</property>
-  <property name="type">GTK_WINDOW_TOPLEVEL</property>
-  <property name="window_position">GTK_WIN_POS_CENTER</property>
-  <property name="modal">True</property>
-  <property name="resizable">False</property>
-  <property name="destroy_with_parent">False</property>
-  <property name="decorated">True</property>
-  <property name="skip_taskbar_hint">False</property>
-  <property name="skip_pager_hint">False</property>
-  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
-  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
-  <property name="has_separator">True</property>
-
-  <child internal-child="vbox">
-    <widget class="GtkVBox" id="dialog-vbox1">
-      <property name="visible">True</property>
-      <property name="homogeneous">False</property>
-      <property name="spacing">0</property>
-
-      <child internal-child="action_area">
-       <widget class="GtkHButtonBox" id="dialog-action_area1">
-         <property name="visible">True</property>
-         <property name="layout_style">GTK_BUTTONBOX_END</property>
 
          <child>
-           <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+           <widget class="GtkFrame" id="frame1">
              <property name="visible">True</property>
-             <property name="can_default">True</property>
-             <property name="can_focus">True</property>
-             <property name="label">gtk-cancel</property>
-             <property name="use_stock">True</property>
-             <property name="relief">GTK_RELIEF_NORMAL</property>
-             <property name="focus_on_click">True</property>
-             <property name="response_id">-6</property>
-           </widget>
-         </child>
+             <property name="label_xalign">0</property>
+             <property name="label_yalign">0</property>
+             <property name="shadow_type">GTK_SHADOW_NONE</property>
 
-         <child>
-           <widget class="GtkButton" id="ConfirmationDialogOkButton">
-             <property name="visible">True</property>
-             <property name="can_default">True</property>
-             <property name="can_focus">True</property>
-             <property name="label">gtk-ok</property>
+             <child>
+               <widget class="GtkNotebook" id="mathOrListNotebook">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="show_tabs">True</property>
+                 <property name="show_border">True</property>
+                 <property name="tab_pos">GTK_POS_TOP</property>
+                 <property name="scrollable">False</property>
+                 <property name="enable_popup">False</property>
+
+                 <child>
+                   <widget class="GtkScrolledWindow" id="ScrolledBrowser">
+                     <property name="visible">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                     <property name="shadow_type">GTK_SHADOW_NONE</property>
+                     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                     <child>
+                       <placeholder/>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="tab_expand">False</property>
+                     <property name="tab_fill">True</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkLabel" id="mathLabel">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">MathView</property>
+                     <property name="use_underline">False</property>
+                     <property name="use_markup">False</property>
+                     <property name="justify">GTK_JUSTIFY_LEFT</property>
+                     <property name="wrap">False</property>
+                     <property name="selectable">False</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xpad">0</property>
+                     <property name="ypad">0</property>
+                   </widget>
+                   <packing>
+                     <property name="type">tab</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkScrolledWindow" id="scrolledwindow9">
+                     <property name="visible">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                     <property name="shadow_type">GTK_SHADOW_IN</property>
+                     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                     <child>
+                       <widget class="GtkTreeView" id="whelpResultTreeview">
+                         <property name="visible">True</property>
+                         <property name="can_focus">True</property>
+                         <property name="headers_visible">False</property>
+                         <property name="rules_hint">False</property>
+                         <property name="reorderable">False</property>
+                         <property name="enable_search">True</property>
+                       </widget>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="tab_expand">False</property>
+                     <property name="tab_fill">True</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkLabel" id="listLabel">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">WhelpResults</property>
+                     <property name="use_underline">False</property>
+                     <property name="use_markup">False</property>
+                     <property name="justify">GTK_JUSTIFY_LEFT</property>
+                     <property name="wrap">False</property>
+                     <property name="selectable">False</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xpad">0</property>
+                     <property name="ypad">0</property>
+                   </widget>
+                   <packing>
+                     <property name="type">tab</property>
+                   </packing>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">True</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+       </widget>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkDialog" id="ConfirmationDialog">
+  <property name="title" translatable="yes">DUMMY</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_CENTER</property>
+  <property name="modal">True</property>
+  <property name="resizable">False</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="has_separator">True</property>
+
+  <child internal-child="vbox">
+    <widget class="GtkVBox" id="dialog-vbox1">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child internal-child="action_area">
+       <widget class="GtkHButtonBox" id="dialog-action_area1">
+         <property name="visible">True</property>
+         <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+         <child>
+           <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-cancel</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
+             <property name="response_id">-6</property>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkButton" id="ConfirmationDialogOkButton">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-ok</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
              <property name="focus_on_click">True</property>
@@ -1037,698 +1221,612 @@ Copyright (C) 2005,
 
              <child>
                <widget class="GtkHandleBox" id="handlebox7">
+                 <property name="border_width">2</property>
                  <property name="visible">True</property>
                  <property name="shadow_type">GTK_SHADOW_OUT</property>
                  <property name="handle_position">GTK_POS_TOP</property>
-                 <property name="snap_edge">GTK_POS_TOP</property>
+                 <property name="snap_edge">GTK_POS_LEFT</property>
 
                  <child>
-                   <widget class="GtkVBox" id="ToolBarVBox">
-                     <property name="width_request">109</property>
+                   <widget class="GtkTable" id="ToolBarTable">
                      <property name="visible">True</property>
-                     <property name="homogeneous">True</property>
-                     <property name="spacing">0</property>
+                     <property name="n_rows">17</property>
+                     <property name="n_columns">2</property>
+                     <property name="homogeneous">False</property>
+                     <property name="row_spacing">4</property>
+                     <property name="column_spacing">0</property>
 
                      <child>
-                       <widget class="GtkVBox" id="vbox10">
+                       <widget class="GtkButton" id="applyButton">
+                         <property name="width_request">50</property>
                          <property name="visible">True</property>
-                         <property name="homogeneous">False</property>
-                         <property name="spacing">0</property>
-
-                         <child>
-                           <widget class="GtkToolbar" id="toolbar11">
-                             <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem4">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="introsButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Intros</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">intros</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem5">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="applyButton">
-                                     <property name="width_request">50</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Apply</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">apply</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
-                           </packing>
-                         </child>
-
-                         <child>
-                           <widget class="GtkToolbar" id="toolbar12">
-                             <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem6">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="exactButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Exact</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">exact</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
-                           </packing>
-                         </child>
+                         <property name="tooltip" translatable="yes">Apply</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">apply</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">0</property>
+                         <property name="bottom_attach">1</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkToolbar" id="toolbar3">
+                       <widget class="GtkButton" id="introsButton">
+                         <property name="width_request">55</property>
                          <property name="visible">True</property>
-                         <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                         <property name="tooltips">True</property>
-                         <property name="show_arrow">True</property>
+                         <property name="tooltip" translatable="yes">Intros</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">intros</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">0</property>
+                         <property name="bottom_attach">1</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem7">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="exactButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Exact</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">exact</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">2</property>
+                         <property name="bottom_attach">3</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="elimButton">
-                                 <property name="width_request">55</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Elim</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">elim</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="elimButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Elim</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">elim</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_HALF</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">4</property>
+                         <property name="bottom_attach">5</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem8">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="reflexivityButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Reflexivity</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">refl</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">8</property>
+                         <property name="bottom_attach">9</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="elimTypeButton">
-                                 <property name="width_request">55</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">ElimType</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">elimTy</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="symmetryButton">
+                         <property name="width_request">50</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Symmetry</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">sym</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">8</property>
+                         <property name="bottom_attach">9</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkToolbar" id="toolbar4">
+                       <widget class="GtkButton" id="transitivityButton">
+                         <property name="width_request">55</property>
                          <property name="visible">True</property>
-                         <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                         <property name="tooltips">True</property>
-                         <property name="show_arrow">True</property>
+                         <property name="tooltip" translatable="yes">Transitivity</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">trans</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">9</property>
+                         <property name="bottom_attach">10</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem9">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="simplifyButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Simplify</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">simpl</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">11</property>
+                         <property name="bottom_attach">12</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="splitButton">
-                                 <property name="width_request">25</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Split</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">∧</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="reduceButton">
+                         <property name="width_request">50</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Reduce</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">red</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">11</property>
+                         <property name="bottom_attach">12</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem10">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="whdButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Whd</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">whd</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">12</property>
+                         <property name="bottom_attach">13</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="leftButton">
-                                 <property name="width_request">25</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Left</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">L</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="assumptionButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Assumption</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">assum</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">14</property>
+                         <property name="bottom_attach">15</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem11">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="autoButton">
+                         <property name="width_request">50</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Auto</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">auto</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">14</property>
+                         <property name="bottom_attach">15</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="rightButton">
-                                 <property name="width_request">25</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Right</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">R</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="cutButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Cut</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">cut</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">16</property>
+                         <property name="bottom_attach">17</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                         <child>
-                           <widget class="GtkToolItem" id="toolitem12">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                     <child>
+                       <widget class="GtkButton" id="replaceButton">
+                         <property name="width_request">50</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">Replace</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">repl</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">16</property>
+                         <property name="bottom_attach">17</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="existsButton">
-                                 <property name="width_request">25</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Exists</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">∃</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
-                         </child>
+                     <child>
+                       <widget class="GtkButton" id="elimTypeButton">
+                         <property name="width_request">55</property>
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">ElimType</property>
+                         <property name="can_focus">True</property>
+                         <property name="label" translatable="yes">elimTy</property>
+                         <property name="use_underline">True</property>
+                         <property name="relief">GTK_RELIEF_NORMAL</property>
+                         <property name="focus_on_click">True</property>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">4</property>
+                         <property name="bottom_attach">5</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options"></property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkVBox" id="vbox12">
+                       <widget class="GtkHBox" id="hbox18">
                          <property name="visible">True</property>
                          <property name="homogeneous">False</property>
                          <property name="spacing">0</property>
 
                          <child>
-                           <widget class="GtkToolbar" id="toolbar5">
+                           <widget class="GtkButton" id="rightButton">
+                             <property name="width_request">25</property>
                              <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem14">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="reflexivityButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Reflexivity</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">refl</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem15">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="symmetryButton">
-                                     <property name="width_request">50</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Symmetry</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">sym</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
+                             <property name="tooltip" translatable="yes">Right</property>
+                             <property name="can_focus">True</property>
+                             <property name="label" translatable="yes">R</property>
+                             <property name="use_underline">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
                            </widget>
                            <packing>
                              <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
+                             <property name="expand">True</property>
+                             <property name="fill">True</property>
                            </packing>
                          </child>
 
                          <child>
-                           <widget class="GtkToolbar" id="toolbar9">
+                           <widget class="GtkButton" id="existsButton">
+                             <property name="width_request">25</property>
                              <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem16">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="transitivityButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Transitivity</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">trans</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
+                             <property name="tooltip" translatable="yes">Exists</property>
+                             <property name="can_focus">True</property>
+                             <property name="label" translatable="yes">∃</property>
+                             <property name="use_underline">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
                            </widget>
                            <packing>
                              <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
+                             <property name="expand">True</property>
+                             <property name="fill">True</property>
                            </packing>
                          </child>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">1</property>
+                         <property name="right_attach">2</property>
+                         <property name="top_attach">6</property>
+                         <property name="bottom_attach">7</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options">fill</property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkVBox" id="vbox11">
+                       <widget class="GtkHBox" id="hbox17">
                          <property name="visible">True</property>
                          <property name="homogeneous">False</property>
                          <property name="spacing">0</property>
 
                          <child>
-                           <widget class="GtkToolbar" id="toolbar8">
+                           <widget class="GtkButton" id="splitButton">
+                             <property name="width_request">25</property>
                              <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem22">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="simplifyButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Simplify</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">simpl</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem23">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="reduceButton">
-                                     <property name="width_request">50</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Reduce</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">red</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
+                             <property name="tooltip" translatable="yes">Split</property>
+                             <property name="can_focus">True</property>
+                             <property name="label" translatable="yes">∧</property>
+                             <property name="use_underline">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
                            </widget>
                            <packing>
                              <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
+                             <property name="expand">True</property>
+                             <property name="fill">True</property>
                            </packing>
                          </child>
 
                          <child>
-                           <widget class="GtkToolbar" id="toolbar10">
+                           <widget class="GtkButton" id="leftButton">
+                             <property name="width_request">25</property>
                              <property name="visible">True</property>
-                             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                             <property name="tooltips">True</property>
-                             <property name="show_arrow">True</property>
-
-                             <child>
-                               <widget class="GtkToolItem" id="toolitem24">
-                                 <property name="visible">True</property>
-                                 <property name="visible_horizontal">True</property>
-                                 <property name="visible_vertical">True</property>
-                                 <property name="is_important">False</property>
-
-                                 <child>
-                                   <widget class="GtkButton" id="whdButton">
-                                     <property name="width_request">55</property>
-                                     <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">Whd</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="label" translatable="yes">whd</property>
-                                     <property name="use_underline">True</property>
-                                     <property name="relief">GTK_RELIEF_NORMAL</property>
-                                     <property name="focus_on_click">True</property>
-                                   </widget>
-                                 </child>
-                               </widget>
-                               <packing>
-                                 <property name="expand">False</property>
-                                 <property name="homogeneous">False</property>
-                               </packing>
-                             </child>
+                             <property name="tooltip" translatable="yes">Left</property>
+                             <property name="can_focus">True</property>
+                             <property name="label" translatable="yes">L</property>
+                             <property name="use_underline">True</property>
+                             <property name="relief">GTK_RELIEF_NORMAL</property>
+                             <property name="focus_on_click">True</property>
                            </widget>
                            <packing>
                              <property name="padding">0</property>
-                             <property name="expand">False</property>
-                             <property name="fill">False</property>
+                             <property name="expand">True</property>
+                             <property name="fill">True</property>
                            </packing>
                          </child>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">6</property>
+                         <property name="bottom_attach">7</property>
+                         <property name="x_options">fill</property>
+                         <property name="y_options">fill</property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkToolbar" id="toolbar6">
+                       <widget class="GtkAlignment" id="alignment6">
                          <property name="visible">True</property>
-                         <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                         <property name="tooltips">True</property>
-                         <property name="show_arrow">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
 
                          <child>
-                           <widget class="GtkToolItem" id="toolitem17">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
-
-                             <child>
-                               <widget class="GtkButton" id="assumptionButton">
-                                 <property name="width_request">55</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Assumption</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">assum</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
+                           <placeholder/>
                          </child>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">1</property>
+                         <property name="bottom_attach">2</property>
+                         <property name="x_options">fill</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkAlignment" id="alignment7">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
 
                          <child>
-                           <widget class="GtkToolItem" id="toolitem18">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                           <placeholder/>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">3</property>
+                         <property name="bottom_attach">4</property>
+                         <property name="x_options">fill</property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="autoButton">
-                                 <property name="width_request">50</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Auto</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">auto</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
+                     <child>
+                       <widget class="GtkAlignment" id="alignment8">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
+
+                         <child>
+                           <placeholder/>
                          </child>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">5</property>
+                         <property name="bottom_attach">6</property>
+                         <property name="x_options">fill</property>
                        </packing>
                      </child>
 
                      <child>
-                       <widget class="GtkToolbar" id="toolbar7">
+                       <widget class="GtkAlignment" id="alignment9">
                          <property name="visible">True</property>
-                         <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
-                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                         <property name="tooltips">True</property>
-                         <property name="show_arrow">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
 
                          <child>
-                           <widget class="GtkToolItem" id="toolitem20">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                           <placeholder/>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">7</property>
+                         <property name="bottom_attach">8</property>
+                         <property name="x_options">fill</property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="cutButton">
-                                 <property name="width_request">55</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Cut</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">cut</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
+                     <child>
+                       <widget class="GtkAlignment" id="alignment10">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
+
+                         <child>
+                           <placeholder/>
                          </child>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">10</property>
+                         <property name="bottom_attach">11</property>
+                         <property name="x_options">fill</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkAlignment" id="alignment11">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
 
                          <child>
-                           <widget class="GtkToolItem" id="toolitem21">
-                             <property name="visible">True</property>
-                             <property name="visible_horizontal">True</property>
-                             <property name="visible_vertical">True</property>
-                             <property name="is_important">False</property>
+                           <placeholder/>
+                         </child>
+                       </widget>
+                       <packing>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">13</property>
+                         <property name="bottom_attach">14</property>
+                         <property name="x_options">fill</property>
+                       </packing>
+                     </child>
 
-                             <child>
-                               <widget class="GtkButton" id="replaceButton">
-                                 <property name="width_request">50</property>
-                                 <property name="visible">True</property>
-                                 <property name="tooltip" translatable="yes">Replace</property>
-                                 <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">repl</property>
-                                 <property name="use_underline">True</property>
-                                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                                 <property name="focus_on_click">True</property>
-                               </widget>
-                             </child>
-                           </widget>
-                           <packing>
-                             <property name="expand">False</property>
-                             <property name="homogeneous">False</property>
-                           </packing>
+                     <child>
+                       <widget class="GtkAlignment" id="alignment12">
+                         <property name="visible">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">1</property>
+                         <property name="yscale">1</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
+
+                         <child>
+                           <placeholder/>
                          </child>
                        </widget>
                        <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
+                         <property name="left_attach">0</property>
+                         <property name="right_attach">1</property>
+                         <property name="top_attach">15</property>
+                         <property name="bottom_attach">16</property>
+                         <property name="x_options">fill</property>
                        </packing>
                      </child>
                    </widget>
@@ -1736,7 +1834,7 @@ Copyright (C) 2005,
                </widget>
                <packing>
                  <property name="padding">0</property>
-                 <property name="expand">True</property>
+                 <property name="expand">False</property>
                  <property name="fill">True</property>
                </packing>
              </child>
@@ -2166,7 +2264,7 @@ Copyright (C) 2005,
              <child>
                <widget class="GtkStatusbar" id="StatusBar">
                  <property name="visible">True</property>
-                 <property name="has_resize_grip">True</property>
+                 <property name="has_resize_grip">False</property>
                </widget>
                <packing>
                  <property name="padding">0</property>
@@ -2440,7 +2538,7 @@ Copyright (C) 2005,
     <widget class="GtkVBox" id="dialog-vbox3">
       <property name="visible">True</property>
       <property name="homogeneous">False</property>
-      <property name="spacing">0</property>
+      <property name="spacing">4</property>
 
       <child internal-child="action_area">
        <widget class="GtkHButtonBox" id="dialog-action_area3">
@@ -2546,7 +2644,19 @@ Copyright (C) 2005,
          </child>
 
          <child>
-           <widget class="GtkButton" id="UriChoiceAutoButton">
+           <widget class="GtkButton" id="copyButton">
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-copy</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
+             <property name="response_id">0</property>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkButton" id="uriChoiceAutoButton">
              <property name="visible">True</property>
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
@@ -2555,7 +2665,7 @@ Copyright (C) 2005,
              <property name="response_id">0</property>
 
              <child>
-               <widget class="GtkAlignment" id="alignment1">
+               <widget class="GtkAlignment" id="alignment5">
                  <property name="visible">True</property>
                  <property name="xalign">0.5</property>
                  <property name="yalign">0.5</property>
@@ -2567,13 +2677,13 @@ Copyright (C) 2005,
                  <property name="right_padding">0</property>
 
                  <child>
-                   <widget class="GtkHBox" id="hbox1">
+                   <widget class="GtkHBox" id="hbox16">
                      <property name="visible">True</property>
                      <property name="homogeneous">False</property>
                      <property name="spacing">2</property>
 
                      <child>
-                       <widget class="GtkImage" id="image18">
+                       <widget class="GtkImage" id="image302">
                          <property name="visible">True</property>
                          <property name="stock">gtk-ok</property>
                          <property name="icon_size">4</property>
@@ -2590,9 +2700,9 @@ Copyright (C) 2005,
                      </child>
 
                      <child>
-                       <widget class="GtkLabel" id="label1">
+                       <widget class="GtkLabel" id="okLabel">
                          <property name="visible">True</property>
-                         <property name="label" translatable="yes">_Auto</property>
+                         <property name="label" translatable="yes">bla bla bla</property>
                          <property name="use_underline">True</property>
                          <property name="use_markup">False</property>
                          <property name="justify">GTK_JUSTIFY_LEFT</property>
@@ -2628,7 +2738,7 @@ Copyright (C) 2005,
        <widget class="GtkVBox" id="vbox2">
          <property name="visible">True</property>
          <property name="homogeneous">False</property>
-         <property name="spacing">0</property>
+         <property name="spacing">3</property>
 
          <child>
            <widget class="GtkLabel" id="UriChoiceLabel">
@@ -2653,10 +2763,11 @@ Copyright (C) 2005,
 
          <child>
            <widget class="GtkScrolledWindow" id="scrolledwindow1">
+             <property name="width_request">400</property>
              <property name="visible">True</property>
              <property name="can_focus">True</property>
-             <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
-             <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+             <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
              <property name="shadow_type">GTK_SHADOW_NONE</property>
              <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
@@ -2679,7 +2790,7 @@ Copyright (C) 2005,
          </child>
 
          <child>
-           <widget class="GtkHBox" id="hbox2">
+           <widget class="GtkHBox" id="uriEntryHBox">
              <property name="visible">True</property>
              <property name="homogeneous">False</property>
              <property name="spacing">0</property>
index 3f08dd1c8f85f2410bda535ee3767e75eaa62c18..cf7939fa7c7ce10300751c9db2a17e3e0dc42492 100644 (file)
@@ -63,6 +63,15 @@ let script =
     ~buffer:gui#main#scriptTextView#buffer
     ~init:(Lazy.force MatitaEngine.initial_status) 
     ~mathviewer:(MatitaMathView.mathViewer ())
+    ~urichooser:(fun uris ->
+      try
+        MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+        ~title:"Matita: URI chooser" 
+        ~msg:"Select the URI" ~hide_uri_entry:true
+        ~hide_try:true ~ok_label:"_Apply" 
+        ~copy_cb:(fun s -> gui#main#scriptTextView#buffer#insert ("\n"^s^"\n"))
+        () ~id:"boh?" uris
+      with MatitaTypes.Cancel -> [])
     ()
 
   (* math viewers *)
@@ -70,7 +79,7 @@ let _ =
   let sequent_viewer = MatitaMathView.sequentViewer_instance () in
   let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
   sequent_viewer#set_href_callback
-    (Some (fun uri -> (MatitaMathView.cicBrowser ())#loadUri uri));
+    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri uri)));
   let browser_observer _ = MatitaMathView.refresh_all_browsers () in
   let sequents_observer status =
     sequents_viewer#reset;
@@ -149,13 +158,13 @@ let _ =
        print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
   (try
-     script#loadFrom Sys.argv.(1);
+     gui#loadScript Sys.argv.(1);
    with Invalid_argument _ -> ());
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
     try
-      browser#loadUri Sys.argv.(1)
+      browser#load (`Uri Sys.argv.(1))
     with Invalid_argument _ -> ()
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
index 30a8b535536e679fe8e3dda4ad33a9f5503e9afa..62f13367539deb44234e01007a56c025b7720bbb 100644 (file)
@@ -12,6 +12,9 @@ TODO
 - spostare il codice di creazione delle tabelle da
   MatitaDb, al momento quelle create da matita possono
   andare out of sync con quelle create dai file .sql
+- commenti exeguibili (forse devono essere una lista e non 
+  un singolo executable e forse devono contenere anche Note 
+  e non solo Executable
 
 DONE
 - tree update in background                              -> Gares
index 59d1c7b79891464d51348e9136716dadd4fd5303..437fed32db9ee9f749c3e7c688cccb15761e3669 100644 (file)
@@ -57,8 +57,12 @@ let tactic_of_ast = function
   | TacticAst.LetIn of 'term * 'ident
   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
   | TacticAst.Replace_pattern of 'term pattern * 'term
-  | TacticAst.Rewrite of direction * 'term * 'ident option
 *)
+  | TacticAst.Rewrite (_,dir,t,ident) ->
+      if dir = `Left then
+        EqualityTactics.rewrite_tac ~term:t 
+      else
+        EqualityTactics.rewrite_back_tac ~term:t
   | _ -> assert false
 
 let eval_tactical status tac =
@@ -200,14 +204,21 @@ let eval_command status cmd =
               (DisambiguateTypes.Num instance) 
               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 
-let eval status st =
-  match st with
+let eval_executable status ex =
+  match ex with
   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
   | TacticAst.Command (_, cmd) -> eval_command status cmd
   | TacticAst.Macro (_, mac) -> 
       command_error (sprintf "The macro %s can't be in a script" 
         (TacticAstPp.pp_macro_cic mac))
 
+let eval_comment status c = status
+            
+let eval status st =
+  match st with
+  | TacticAst.Executable (_,ex) -> eval_executable status ex
+  | TacticAst.Comment (_,c) -> eval_comment status c
+
 let disambiguate_term status term =
   let (aliases, metasenv, cic, _) =
     match
@@ -283,8 +294,10 @@ let disambiguate_tactic status = function
   | TacticAst.LetIn of 'term * 'ident
   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
   | TacticAst.Replace_pattern of 'term pattern * 'term
-  | TacticAst.Rewrite of direction * 'term * 'ident option
 *)
+  | TacticAst.Rewrite (loc,dir,t,ident) ->
+      let status, term = disambiguate_term status t in
+      status, TacticAst.Rewrite (loc,dir,term,ident)
   | TacticAst.Intros (loc, num, names) ->
       status, TacticAst.Intros (loc, num, names)
   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
@@ -430,8 +443,8 @@ let disambiguate_command status = function
       status, cmd
   | TacticAst.Alias _ as x -> status, x
 
-let disambiguate_statement status statement =
-  match statement with
+let disambiguate_executable status ex =
+  match ex with
   | TacticAst.Tactical (loc, tac) ->
       let status, tac = disambiguate_tactical status tac in
       status, (TacticAst.Tactical (loc, tac))
@@ -442,6 +455,22 @@ let disambiguate_statement status statement =
       command_error 
         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
+
+let disambiguate_comment status c = 
+  match c with
+  | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
+  | TacticAst.Code (loc,ex) -> 
+        let status, ex = disambiguate_executable status ex in
+        status, TacticAst.Code (loc,ex)
+        
+let disambiguate_statement status statement =
+  match statement with
+  | TacticAst.Comment (loc,c) -> 
+        let status, c = disambiguate_comment status c in
+        status, TacticAst.Comment (loc,c)
+  | TacticAst.Executable (loc,ex) -> 
+        let status, ex = disambiguate_executable status ex in
+        status, TacticAst.Executable (loc,ex)
   
 let eval_ast status ast =
   let status,st = disambiguate_statement status ast in
index 274ee123a2a9ba48e38d5bd811a7317f16ed0586..0301b31f2e3981a02aad48493943af7a04c03223 100644 (file)
@@ -39,6 +39,9 @@ let wrap_callback f () =
 let connect_button (button: #GButton.button) callback =
   ignore (button#connect#clicked (wrap_callback callback))
 
+let connect_toggle_button (button: #GButton.toggle_button) callback =
+  ignore (button#connect#toggled (wrap_callback callback))
+
 let connect_menu_item (menu_item: #GMenu.menu_item) callback =
   ignore (menu_item#connect#activate (wrap_callback callback))
 
index 23f820f86b21208b346f57534e41dab6289b6fc7..993dff4c37c0f74b82dace32a85b8c117b7d70c1 100644 (file)
@@ -39,6 +39,11 @@ val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
   * value *)
 val connect_button: #GButton.button -> (unit -> unit) -> unit
 
+
+(** Connect a callback to the toggled signal of a button, ignoring its return
+  * value *)
+val connect_toggle_button: #GButton.toggle_button -> (unit -> unit) -> unit
+
 (** Like connect_button above, but connects a callback to the activate signal of
   * a menu item *)
 val connect_menu_item: #GMenu.menu_item -> (unit -> unit) -> unit
index ec4d042ff38223eb61cd6151c84b7f19171c8d99..5045f36d1aa5148bd3ec80c2f3c3a7fa4b46ed26 100644 (file)
@@ -63,7 +63,8 @@ class gui () =
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
-
+    val mutable script_fname = None 
+   
     initializer
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
@@ -155,33 +156,37 @@ class gui () =
              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
         (* script *)
       let s () = MatitaScript.instance () in
-      let script_fname = ref None in
-      let enable_save_to f =
-        script_fname := Some f;
-        self#main#saveMenuItem#misc#set_sensitive true
-      in
-      let disable_save () =
-        script_fname := None;
+      let disableSave () =
+        script_fname <- None;
         self#main#saveMenuItem#misc#set_sensitive false
       in
       let loadScript () =
         let script = s () in
         match self#chooseFile () with
-        | Some f -> script#reset (); script#loadFrom f; enable_save_to f
+        | Some f -> 
+              script#reset (); 
+              script#loadFrom f; 
+              console#message ("'"^f^"' loaded.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveAsScript () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
-        | Some f -> script#saveTo f; enable_save_to f
+        | Some f -> 
+              script#saveTo f; 
+              console#message ("'"^f^"' saved.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveScript () =
-        match !script_fname with
+        match script_fname with
         | None -> saveAsScript ()
-        | Some f -> (s ())#saveTo f
+        | Some f -> 
+              (s ())#saveTo f;
+              console#message ("'"^f^"' saved.");
       in
-      let newScript () = (s ())#reset (); disable_save () in
+      let newScript () = (s ())#reset (); disableSave () in
       let cursor () =
         let buf = self#main#scriptTextView#buffer in
         buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
@@ -228,6 +233,18 @@ class gui () =
       self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
         (* focus *)
       self#main#scriptTextView#misc#grab_focus ()
+    
+    method loadScript file =       
+      let script = MatitaScript.instance () in
+      script#reset (); 
+      script#loadFrom file; 
+      console#message ("'"^file^"' loaded.");
+      self#_enableSaveTo file
+        
+    method private _enableSaveTo file =
+      script_fname <- Some file;
+      self#main#saveMenuItem#misc#set_sensitive true
+        
 
     method console = console
 
@@ -237,6 +254,30 @@ class gui () =
 
     method newBrowserWin () =
       let win = new browserWin () in
+      win#whelpImage2#set_file "icons/whelp.png";
+      win#whelpBarToggleButton#set_active false;   
+      win#whelpBarBox#misc#hide ();
+      win#mathOrListNotebook#set_show_tabs false;
+      connect_toggle_button win#whelpBarToggleButton 
+        (fun () -> 
+          if win#whelpBarToggleButton#active then
+            win#whelpBarBox#misc#show ()
+          else
+            win#whelpBarBox#misc#hide ());
+      let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
+      let combo,(combo_store,combo_column) = 
+        GEdit.combo_box_text ~strings:queries () 
+      in
+      combo#set_active 0;
+      win#comboVbox#add (combo :> GObj.widget);
+      let start_query () = 
+        let query = String.lowercase (List.nth queries combo#active) in
+        let input = win#queryInputText#text in
+        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
+        (MatitaScript.instance ())#advance ~statement ()
+      in
+      ignore(win#queryInputText#connect#activate ~callback:start_query);
+      ignore(combo#connect#changed ~callback:start_query);
       win#check_widgets ();
       win
 
@@ -312,7 +353,8 @@ let is_var_uri s =
 
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
-  ?(msg = "") ?(nonvars_button = false) ()
+  ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
+  ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
   ~id uris
 =
   let gui = instance () in
@@ -323,11 +365,28 @@ let interactive_uri_choice
     Lazy.force nonvars_uris
   else begin
     let dialog = gui#newUriDialog () in
+    if hide_uri_entry then
+      dialog#uriEntryHBox#misc#hide ();
+    if hide_try then
+      begin
+      dialog#uriChoiceSelectedButton#misc#hide ();
+      dialog#uriChoiceConstantsButton#misc#hide ();
+      end;
+    dialog#okLabel#set_label ok_label;  
     dialog#uriChoiceTreeView#selection#set_mode
       (selection_mode :> Gtk.Tags.selection_mode);
     let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
     let nonvars = ref false in
+    (match copy_cb with
+    | None -> ()
+    | Some cb ->
+        dialog#copyButton#misc#show ();
+        connect_button dialog#copyButton 
+        (fun _ ->
+          match model#easy_selection () with
+          | [u] -> (cb u)
+          | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
     List.iter model#easy_append uris;
index aabcba1e8805441cd1c6cdd5bd1327e9ae91a4d9..cb2cbeb0c00ef46775cb549b4d54b8d62d7d538c 100644 (file)
@@ -69,6 +69,8 @@ object
     (** prompt the user for a (multiline) text entry *)
   method askText: ?title:string -> ?msg:string -> unit -> string option
 
+  method loadScript: string -> unit
+                                                            
 end
 
   (** singleton instance of the gui *)
@@ -84,7 +86,9 @@ val instance: unit -> gui
     * @raise MatitaTypes.Cancel *)
 val interactive_uri_choice:
   ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
-  ?msg:string -> ?nonvars_button:bool -> unit ->
+  ?msg:string -> ?nonvars_button:bool -> 
+  ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
+  ?copy_cb:(string -> unit) -> unit ->
     MatitaDisambiguator.choose_uris_callback
 
   (** @raise MatitaTypes.Cancel *)
index c9e0b217faf4e0638841b06f940a16273b38931e..1f18e76a6a3aebc46af710b19b85fda96acfd958 100644 (file)
@@ -280,11 +280,14 @@ let cicBrowsers = ref []
 
 class type cicBrowser =
 object
-  method loadUri: string -> unit
-  method loadTerm: term_source -> unit
+  method load: MatitaTypes.mathViewer_entry -> unit
+  method loadList: string list -> MatitaTypes.mathViewer_entry-> unit
+  method loadInput: string -> unit
 end
 
-class cicBrowser_impl ~(history:string MatitaMisc.history) () =
+class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
+  ()
+=
   let term_RE = Pcre.regexp "^term:(.*)" in
   let trailing_slash_RE = Pcre.regexp "/$" in
   let gui = MatitaGui.instance () in
@@ -306,10 +309,12 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () =
     inherit scriptAccessor
 
     initializer
+      win#browserForwardButton#misc#set_sensitive false;
+      win#browserBackButton#misc#set_sensitive false;
       ignore (win#browserUri#connect#activate (handle_error' (fun () ->
-        self#_loadUri win#browserUri#text)));
+        self#loadInput win#browserUri#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
-        self#_loadUri current_proof_uri)));
+        self#_load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
         (handle_error' self#refresh));
       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
@@ -323,107 +328,139 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () =
         then
           GMain.quit ();
         false));
+      ignore(win#whelpResultTreeview#connect#row_activated 
+        ~callback:(fun _ _ ->
+          let old = win#browserUri#text in
+          self#loadInput (old ^ self#_getWhelpResultTreeviewSelection ())));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#_loadUri uri)));
-      self#_loadUri ~add_to_history:false blank_uri;
-      toplevel#show ();
+        handle_error (fun () -> self#_load (`Uri uri))));
+      self#_load (`About `Blank);
+      toplevel#show ()
 
-    val mutable current_uri = ""
+    val mutable current_entry = `About `Blank 
     val mutable current_infos = None
     val mutable current_mathml = None
 
+    val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview
+
+    method private _getWhelpResultTreeviewSelection () =
+      match model#easy_selection () with
+          | [u] -> u
+          | _ -> assert false
+
+    (** history RATIONALE 
+     *
+     * all operations about history are done using _historyFoo
+     *
+     * only toplevel function like load loadList loadInput can call
+     * _historyAdd
+     *)
+          
+    method private _historyAdd item = 
+      history#add item;
+      win#browserBackButton#misc#set_sensitive true;
+      win#browserForwardButton#misc#set_sensitive false
+
+    method private _historyPrev () =
+      let item = history#previous in
+      if history#is_begin then win#browserBackButton#misc#set_sensitive false;
+      win#browserForwardButton#misc#set_sensitive true;
+      item
+    
+    method private _historyNext () =
+      let item = history#next in
+      if history#is_end then win#browserForwardButton#misc#set_sensitive false;
+      win#browserBackButton#misc#set_sensitive true;
+      item
+
+    (** notebook RATIONALE 
+     * 
+     * Use only these functions to switch between the tabs
+     *)
+    method private _showList = win#mathOrListNotebook#goto_page 1
+    method private _showMath = win#mathOrListNotebook#goto_page 0
+    
+
+    
     method private back () =
       try
-        self#_loadUri ~add_to_history:false history#previous
+        self#_load (self#_historyPrev ())
       with MatitaMisc.History_failure -> ()
 
     method private forward () =
       try
-        self#_loadUri ~add_to_history:false history#next
+        self#_load (self#_historyNext ())
       with MatitaMisc.History_failure -> ()
 
       (* loads a uri which can be a cic uri or an about:* uri
       * @param uri string *)
-    method private _loadUri ?(add_to_history = true) uri =
+    method private _load entry =
       try
-        if current_uri <> uri || uri = current_proof_uri then begin
-          (match uri with
-          | uri when uri = blank_uri -> self#blank ()
-          | uri when uri = current_proof_uri -> self#home ()
-          | uri when Pcre.pmatch ~rex:term_RE uri ->
-              self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1))
-          | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri
-          | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri));
-          self#setUri uri;
-          if add_to_history then history#add uri
-        end
+          if entry <> current_entry || entry = `About `Current_proof then begin
+            (match entry with
+            | `About `Current_proof -> self#home ()
+            | `About `Blank -> self#blank ()
+            | `About `Us -> () (* TODO implement easter egg here :-] *)
+            | `Check term -> self#_loadCheck term
+            | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+            | `Dir dir -> self#_loadDir dir
+            | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
+            | `Whelp (query, results) -> self#loadList results entry);
+            self#setEntry entry
+          end
       with
-      | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri)
-      | CicEnvironment.Object_not_found _ ->
-          fail (sprintf "object not found: %s" uri)
+      | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri)
+      | CicEnvironment.Object_not_found uri ->
+          fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
       | Browser_failure msg -> fail msg
 
-    method loadUri uri =
-      handle_error (fun () -> self#_loadUri ~add_to_history:true uri)
 
     method private blank () =
-      mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
+      mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement;
+      self#_showMath
+
+    method private _loadCheck term =
+      failwith "not implemented _loadCheck";
+      self#_showMath
 
     method private home () =
+      self#_showMath;
       match self#script#status.proof_status with
       | Proof  (uri, metasenv, bo, ty) ->
           let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
-          self#loadObj obj
+          self#_loadObj obj
       | Incomplete_proof ((uri, metasenv, bo, ty), _) -> 
           let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
-          self#loadObj obj
+          self#_loadObj obj
       | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
-    method private loadUriManagerUri uri =
+    method private _loadUriManagerUri uri =
       let uri = UriManager.strip_xpointer uri in
       let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      self#loadObj obj
-
-    method private loadDir dir =
-      let mathml = MatitaMisc.empty_boxml () in
+      self#_loadObj obj
+      
+    method private _loadDir dir = 
       let content = Http_getter.ls dir in
-      let root = mathml#get_documentElement in
-      let new_box_elt name =
-        mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns)
-          ~qualifiedName:(Gdome.domString ("b:" ^ name))
+      let l = List.map (function 
+        | Http_getter_types.Ls_section sec -> sec            
+        | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri
+        ) content
       in
-      let new_text content = mathml#createTextNode (Gdome.domString content) in
-      let b_v = new_box_elt "v" in
-      List.iter
-        (fun item ->
-          let b_text = new_box_elt "text" in
-          let uri, elt =
-            match item with
-            | Http_getter_types.Ls_section subdir ->
-                (dir ^ subdir ^ "/"), (new_text (subdir ^ "/"))
-            | Http_getter_types.Ls_object obj ->
-                (dir ^ obj.Http_getter_types.uri),
-                (new_text obj.Http_getter_types.uri)
-          in
-          b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns)
-            ~qualifiedName:(Gdome.domString "xlink:href")
-            ~value:(Gdome.domString uri);
-          ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node));
-          ignore (b_text#appendChild ~newChild:(elt :> Gdome.node)))
-        content;
-      ignore (root#appendChild ~newChild:(b_v :> Gdome.node));
-(*       Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *)
-      mathView#load_root ~root:root
-
-    method private setUri uri =
-        win#browserUri#set_text uri;
-        current_uri <- uri
-
-    method private loadObj obj =
+      self#_loadList l
+
+    method private setEntry entry =
+        win#browserUri#set_text (string_of_entry entry);
+        current_entry <- entry
+
+    method private _loadObj obj =
+      self#_showMath; 
+      (* this must be _before_ loading the document, since 
+       * if the widget is not mapped (hidden by the notebook)
+       * the document is not rendered *)
       let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
       let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
            ids_to_hypotheses,_,_))) =
@@ -431,51 +468,69 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () =
       in
       current_infos <- Some (ids_to_terms, ids_to_father_ids,
         ids_to_conjectures, ids_to_hypotheses);
-      match current_mathml with
+      (match current_mathml with
       | Some current_mathml when use_diff ->
           mathView#freeze;
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
           mathView#load_root ~root:mathml#get_documentElement;
-          current_mathml <- Some mathml
-
-    method private _loadTerm s = failwith "not implemented _loadTerm"
-(* TODO  self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *)
-
-    method private _loadTermAst ast = failwith "not implemented _loadTermAst"
-(* TODO
-      let (_, metasenv, term, _) =
-        MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
-      in
-      self#_loadTermCic term metasenv
-*)
+          current_mathml <- Some mathml);
 
     method private _loadTermCic term metasenv =
       let context = self#script#proofContext in
       let dummyno = CicMkImplicit.new_meta metasenv [] in
       let sequent = (dummyno, context, term) in
-      mathView#load_sequent (sequent :: metasenv) dummyno
-
-    method loadTerm (src:term_source) =
-      handle_error (fun () ->
-        (match src with
-        | `Ast ast -> self#_loadTermAst ast
-        | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv
-        | `String s -> self#_loadTerm s);
-        self#setUri "check")
-
+      mathView#load_sequent (sequent :: metasenv) dummyno;
+      self#_showMath
+
+    method private _loadList l =
+      model#list_store#clear ();
+      List.iter model#easy_append l;
+      self#_showList
+    
+    (** { public methods } *)
+      
+    method load uri =
+      handle_error (fun () -> self#_load uri);
+      self#_historyAdd uri
+
+    method loadList l entry = 
+      self#_loadList l;
+      self#_historyAdd entry
+    
+    method loadInput txt = 
+      let add_terminating_slash s =
+        if s.[String.length s - 1] <> '/' then s^"/" else s
+      in
+      let is_uri = 
+        try 
+          ignore(Http_getter.resolve txt); true
+        with
+        | Http_getter_types.Key_not_found _ 
+        | Http_getter_types.Unresolvable_URI _ -> false
+      in
+      let entry = 
+        if is_uri then
+          (`Uri txt)
+        else
+          (`Dir (add_terminating_slash txt))
+      in
+      self#_load entry;
+      self#_historyAdd entry
+      
+        
       (** {2 methods used by constructor only} *)
 
     method win = win
     method history = history
-    method currentUri = current_uri
+    method currentEntry = current_entry
     method refresh () =
-      if current_uri = current_proof_uri then
-      self#_loadUri ~add_to_history:false current_proof_uri
-
+      if current_entry = `About `Current_proof then
+      self#_load (`About `Current_proof) 
   end
 
+  
 let sequentsViewer ~(notebook:GPack.notebook)
   ~(sequentViewer:sequentViewer) ()
 =
@@ -488,10 +543,11 @@ let cicBrowser () =
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
-        new MatitaMisc.browser_history ~memento:history#save size ""
+        new MatitaMisc.browser_history ~memento:history#save size
+          (`About `Blank)
       in
       let newBrowser = aux history in
-      newBrowser#loadUri browser#currentUri));
+      newBrowser#load browser#currentEntry));
 (*
       (* attempt (failed) to close windows on CTRL-W ... *)
     MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
@@ -500,7 +556,7 @@ let cicBrowser () =
     cicBrowsers := browser :: !cicBrowsers;
     (browser :> cicBrowser)
   in
-  let history = new MatitaMisc.browser_history size blank_uri in
+  let history = new MatitaMisc.browser_history size (`About `Blank) in
   aux history
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
@@ -514,8 +570,18 @@ let default_sequentsViewer () =
   sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
 
-
 let mathViewer () = 
-  object 
-    method show_term t = (cicBrowser ()) # loadTerm t
+  object(self)
+    method private get_browser reuse = 
+      if reuse then
+        (match !cicBrowsers with
+        | [] -> cicBrowser ()
+        | b :: _ -> (b :> cicBrowser))
+      else
+        (cicBrowser ())
+          
+    method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
+      
+    method show_uri_list ?(reuse=false) ~entry l =
+      (self#get_browser reuse)#loadList l entry
   end
index e26352dadb1fbaab7dcc9601cc4e3078d68389aa..1dc3dabe8bcca48af519cc3d3b6d5068cfb5aad4 100644 (file)
@@ -62,8 +62,9 @@ exception Browser_failure of string
 
 class type cicBrowser =
 object
-  method loadUri: string -> unit
-  method loadTerm: MatitaTypes.term_source -> unit
+  method load: MatitaTypes.mathViewer_entry -> unit
+  method loadList: string list -> MatitaTypes.mathViewer_entry -> unit
+  method loadInput: string -> unit
 end
 
 (** {2 Constructors} *)
index 41b96793884d88546a2cd42ce06101551ddeef44..e1c55feb204e02ca0e3c9354d9b1aa7eaa48c2b2 100644 (file)
@@ -76,17 +76,30 @@ class type ['a] history =
     method previous : 'a
     method load: 'a memento -> unit
     method save: 'a memento
+    method is_begin: bool
+    method is_end: bool
   end
 
+class basic_history (head, tail, cur) =
+  object
+    val mutable hd = head  (* insertion point *)
+    val mutable tl = tail (* oldest inserted item *)
+    val mutable cur = cur  (* current item for the history *)
+    
+    method is_begin = cur <= tl
+    method is_end = cur >= hd
+  end
+  
+  
 class shell_history size =
   let size = size + 1 in
   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
   let incr x = (x + 1) mod size in
   object (self)
     val data = Array.create size ""
-    val mutable hd = 0  (* insertion point *)
-    val mutable tl = -1 (* oldest inserted item *)
-    val mutable cur = -1  (* current item for the history *)
+
+    inherit basic_history (0, -1 , -1)
+    
     method add s =
       data.(hd) <- s;
       if tl = -1 then tl <- hd;
@@ -112,9 +125,9 @@ class ['a] browser_history ?memento size init =
   object (self)
     initializer match memento with Some m -> self#load m | _ -> ()
     val data = Array.create size init
-    val mutable hd = 0
-    val mutable tl = 0
-    val mutable cur = 0
+
+    inherit basic_history (0, 0, 0)
+    
     method previous =
       if cur = tl then raise History_failure;
       cur <- cur - 1;
index 4f2905a24873e42f62249047f83b9f7a47afd14a..3731bd1a615204955dbade3806ed6d7e623f37f1 100644 (file)
@@ -59,6 +59,8 @@ class type ['a] history =
     method previous : 'a    (** @raise History_failure *)
     method load: 'a memento -> unit
     method save: 'a memento
+    method is_begin: bool 
+    method is_end: bool 
   end
 
   (** shell like history: new items added at the end of the history
index c64653c798bde6e90382880bd5070e060657e260..fed62fbb321c4e73b45a4b59b82e0e9c017386f9 100644 (file)
@@ -34,8 +34,16 @@ let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
 
 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
-let blanks_RE = Pcre.regexp "^\\s*$"
-
+let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
+let multiline_RE = Pcre.regexp "^\n[^\n]+$"
+let newline_RE = Pcre.regexp "\n"
+let comment str =
+  if Pcre.pmatch ~rex:multiline_RE str then
+    "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " **)"
+  else
+    "\n(**\n" ^ str ^ "\n**)"
+                     
 let first_line s =
   let s = Pcre.replace ~rex:heading_nl_RE s in
   try
@@ -53,109 +61,173 @@ let prepend_text header base =
 let goal_ast n =
   let module A = TacticAst in
   let loc = CicAst.dummy_floc in
-  A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))
-
-let eval_statement status mathviewer user_goal s =
-  let st = CicTextualParser2.parse_statement (Stream.of_string s) in
-  match st with
-  | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) ->
-      let parsed_text_length = snd (CicAst.loc_of_floc loc) in
-      let parsed_text = safe_substring s 0 parsed_text_length in
-      let goal_changed = ref false in
-      let status =
-        match status.proof_status with
-        | Incomplete_proof (_, goal) when goal <> user_goal ->
-            goal_changed := true;
-            MatitaEngine.eval_ast status (goal_ast user_goal)
-        | _ -> status
-      in
-      let new_status = MatitaEngine.eval_ast status st in
-      let new_aliases =
-        match st with
-        | TacticAst.Command (_, TacticAst.Alias _) ->
-            DisambiguateTypes.Environment.empty
-        | _ -> MatitaSync.alias_diff ~from:status new_status
-      in
-      let new_text =
-        if DisambiguateTypes.Environment.is_empty new_aliases then
-          parsed_text
-        else
-          prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
-            parsed_text
-      in
-      let new_text =
-        if !goal_changed then
-          prepend_text
-            (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*))
-            new_text
-        else
-          new_text
+  A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
+
+let eval_with_engine status user_goal parsed_text st =
+  let module TA = TacticAst in
+  let module TAPp = TacticAstPp in
+  let parsed_text_length = String.length parsed_text in
+  let loc, ex = 
+    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false 
+  in
+  let goal_changed = ref false in
+  let status =
+    match status.proof_status with
+      | Incomplete_proof (_, goal) when goal <> user_goal ->
+          goal_changed := true;
+          MatitaEngine.eval_ast status (goal_ast user_goal)
+      | _ -> status
+  in
+  let new_status = MatitaEngine.eval_ast status st in
+  let new_aliases =
+    match ex with
+      | TA.Command (_, TA.Alias _) ->
+          DisambiguateTypes.Environment.empty
+      | _ -> MatitaSync.alias_diff ~from:status new_status
+  in
+  let new_text =
+    if DisambiguateTypes.Environment.is_empty new_aliases then
+      parsed_text
+    else
+      prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
+        parsed_text
+  in
+  let new_text =
+    if !goal_changed then
+      prepend_text
+        (TAPp.pp_tactic (TA.Goal (loc, user_goal))(* ^ "\n"*))
+        new_text
+    else
+      new_text
+  in
+    [ new_status, new_text ], parsed_text_length
+let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text mac =
+  let module TA = TacticAst in
+  let module TAPp = TacticAstPp in
+  let module MQ = MetadataQuery in
+  let module MD = MatitaDisambiguator in
+  let module MDB = MatitaDb in
+  let parsed_text_length = String.length parsed_text in
+  match mac with
+  | TA.Hint loc -> 
+      let s = MatitaMisc.get_proof_status status in
+      let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in
+      let selected = urichooser l in
+      (match selected with
+      | [] -> [], parsed_text_length
+      | [uri] -> 
+        let ast = 
+          (TA.Executable (loc,
+            (TA.Tactical (loc, 
+               TA.Tactic (loc,
+                 TA.Apply (loc, CicAst.Uri (uri,None))))))) 
+        in
+        let new_status = MatitaEngine.eval_ast status ast in
+        let extra_text = 
+          comment parsed_text ^ 
+          "\n" ^ TAPp.pp_statement ast
+        in
+        [ new_status , extra_text ],parsed_text_length
+      | _ -> assert false)
+  | TA.Match (_,term) -> 
+      let dbd = MatitaDb.instance () in
+      let metasenv = MatitaMisc.get_proof_metasenv status in
+      let context = MatitaMisc.get_proof_context status in
+      let aliases = MatitaMisc.get_proof_aliases status in
+      let (_env,_metasenv,term,_graph) = 
+        let interps =
+          MD.disambiguate_term dbd context metasenv aliases term 
+        in
+        match interps with 
+        | [x] -> x
+        | _ -> assert false
       in
-      [ new_status, new_text ], parsed_text_length
-  | TacticAst.Macro (loc, mac) ->
-      let parsed_text_length = snd (CicAst.loc_of_floc loc) in
-      (match mac with (* TODO *)
-       | TacticAst.Hint _ -> 
-          let s = MatitaMisc.get_proof_status status in
-          let l = List.map fst
-            (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s) 
-          in
-          List.iter prerr_endline l;
-          prerr_endline "FINITA LA HINT"; assert false
-    | TacticAst.Match (_,term) -> 
-        let dbd = MatitaDb.instance () in
-        let metasenv = MatitaMisc.get_proof_metasenv status in
-        let context = MatitaMisc.get_proof_context status in
-        let aliases = MatitaMisc.get_proof_aliases status in
-        let (_env,_metasenv,term,_graph) = 
-          let interps =
-            MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term 
-          in
-          match interps with 
-          | [x] -> x
-          | _ -> assert false
+      let results =  MetadataQuery.match_term ~dbd:dbd term in
+      mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results))
+        results;
+      [], parsed_text_length
+  | TA.Instance (_,term) ->
+      let dbd = MatitaDb.instance () in
+      let metasenv = MatitaMisc.get_proof_metasenv status in
+      let context = MatitaMisc.get_proof_context status in
+      let aliases = MatitaMisc.get_proof_aliases status in
+      let (_env,_metasenv,term,_graph) = 
+        let interps =
+          MD.disambiguate_term dbd context metasenv aliases term 
         in
-        List.iter prerr_endline (MetadataQuery.match_term ~dbd:dbd term);
-        assert false;
-     | TacticAst.Instance (_,term) ->
-        let dbd = MatitaDb.instance () in
-        let metasenv = MatitaMisc.get_proof_metasenv status in
-        let context = MatitaMisc.get_proof_context status in
-        let aliases = MatitaMisc.get_proof_aliases status in
-        let (_env,_metasenv,term,_graph) = 
-          let interps =
-            MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term 
-          in
           match interps with 
-          | [x] -> x
-          | _ -> assert false
+            | [x] -> x
+            | _ -> assert false
+      in
+      let results = MetadataQuery.instance ~dbd term in
+        mathviewer#show_uri_list ~reuse:true
+          ~entry:(`Whelp ("instance", results)) results;
+        [], parsed_text_length
+          
+
+  | TA.Check (_,t) ->
+      let metasenv = MatitaMisc.get_proof_metasenv status in
+      let context = MatitaMisc.get_proof_context status in
+      let aliases = MatitaMisc.get_proof_aliases status in
+      let db = MatitaDb.instance () in
+      let (_env,_metasenv,term,_graph) = 
+        let interps = 
+          MD.disambiguate_term db context metasenv aliases t 
         in
-        List.iter prerr_endline (MetadataQuery.instance ~dbd term);
-        assert false
-        
-        | TacticAst.Check (_,t) ->
-            let metasenv = MatitaMisc.get_proof_metasenv status in
-            let context = MatitaMisc.get_proof_context status in
-            let aliases = MatitaMisc.get_proof_aliases status in
-            let db = MatitaDb.instance () in
-            let (_env,_metasenv,term,_graph) = 
-              let interps = 
-                MatitaDisambiguator.disambiguate_term db context metasenv aliases t 
-              in
-              match interps with 
-              | [x] -> x
-              | _ -> assert false
-            in
-            let ty,_ = 
-              CicTypeChecker.type_of_aux' metasenv context term
-                CicUniv.empty_ugraph 
-            in
-            mathviewer # show_term (`Cic (ty,metasenv) );
-            [ status, "" ] , parsed_text_length
-       | _ -> failwith "not implemented")
+          match interps with 
+            | [x] -> x
+            | _ -> assert false
+      in
+      let ty,_ = 
+        CicTypeChecker.type_of_aux' metasenv context term
+          CicUniv.empty_ugraph 
+      in
+      let t_and_ty = Cic.Cast (term,ty) in
+        mathviewer # show_entry (`Cic (t_and_ty,metasenv));
+        [], parsed_text_length
+  | TA.Quit _ ->
+      failwith "not implemented quit"
+  | _ -> failwith "not implemented"
+
+                                
+let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text ex =
+  let module TA = TacticAst in
+  let module TAPp = TacticAstPp in
+  let module MD = MatitaDisambiguator in
+  let parsed_text_length = String.length parsed_text in
+  match ex with
+  | TA.Command (loc, _) | TA.Tactical (loc, _) ->
+      eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex))
+  | TA.Macro (_,mac) ->
+      eval_macro status mathviewer urichooser parsed_text mac
+
+let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal s =
+  if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
+  let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+  let text_of_loc loc =
+    let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+    let parsed_text = safe_substring s 0 parsed_text_length in
+    parsed_text, parsed_text_length
+  in
+  match st with
+  | TacticAst.Comment (loc,_)-> 
+      let parsed_text, parsed_text_length = text_of_loc loc in
+      let remain_len = String.length s - parsed_text_length in
+      let s = String.sub s parsed_text_length remain_len in
+      let s,len = eval_statement status mathviewer urichooser user_goal s in
+      (match s with
+      | (status, text) :: tl ->
+        ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
+      | [] -> [], 0)
+  | TacticAst.Executable (loc, ex) ->
+      let parsed_text, parsed_text_length = text_of_loc loc in
+      eval_executable status mathviewer urichooser user_goal parsed_text ex
+  
 
 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) 
-              ~(mathviewer: MatitaTypes.mathViewer) () =
+              ~(mathviewer: MatitaTypes.mathViewer) 
+              ~urichooser () =
 object (self)
   initializer self#reset ()
 
@@ -180,10 +252,9 @@ object (self)
 
   method private _advance ?statement () =
     let s = match statement with Some s -> s | None -> self#getFuture in
-    if Pcre.pmatch ~rex:blanks_RE s then raise Margin;
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
     let (entries, parsed_len) = 
-      eval_statement self#status mathviewer userGoal s in
+      eval_statement self#status mathviewer urichooser userGoal s in
     let (new_statuses, new_statements) = List.split entries in
 (*
 prerr_endline "evalStatement returned";
@@ -317,8 +388,8 @@ end
 
 let _script = ref None
 
-let script ~buffer ~init ~mathviewer () =
-  let s = new script ~buffer ~init ~mathviewer () in
+let script ~buffer ~init ~mathviewer ~urichooser () =
+  let s = new script ~buffer ~init ~mathviewer ~urichooser () in
   _script := Some s;
   s
 
index f7c86fc3c3298a0a79bf9f57edbe89e6be2853da..df3ec4e1e358a840b62096f9420f457d0713d3c1 100644 (file)
@@ -65,6 +65,7 @@ val script:
   buffer:GText.buffer -> 
   init:MatitaTypes.status -> 
   mathviewer: MatitaTypes.mathViewer-> 
+  urichooser: (string list -> string list) -> 
   unit -> 
     script
 
index 454c17a7f521afc53be9b9fc9460d75ba3a4b564..f5ec78ee00c33c4ee29f94f1038b069d4de442aa 100644 (file)
@@ -145,14 +145,37 @@ class type console =
     method show : ?msg:string -> unit -> unit
   end
 
-type term_source =
-  [ `Ast of DisambiguateTypes.term
+type abouts =
+  [ `Blank
+  | `Current_proof
+  | `Us
+  ]
+  
+type mathViewer_entry =
+  [ `About of abouts  (* current proof *)
+  | `Check of string (* term *)
   | `Cic of Cic.term * Cic.metasenv
-  | `String of string
+  | `Dir of string (* "directory" in cic uris namespace *)
+  | `Uri of string (* cic object uri *)
+  | `Whelp of string * string list (* query and results *)
   ]
 
+let string_of_entry = function
+  | `About `Blank -> "about:blank"
+  | `About `Current_proof -> "about:proof"
+  | `About `Us -> "about:us"
+  | `Check _ -> "check:"
+  | `Cic (_, _) -> "term:"
+  | `Dir uri | `Uri uri -> uri
+  | `Whelp (query, _) -> sprintf "whelp:%s" query
+
 class type mathViewer =
   object
-    method show_term: term_source -> unit
+    (** @param reuse if set reused last opened cic browser otherwise 
+     *  opens a new one. default is false
+     *)
+    method show_entry: ?reuse:bool -> mathViewer_entry -> unit
+    method show_uri_list:
+      ?reuse:bool -> entry:mathViewer_entry -> string list -> unit
   end
   
index 4d7b03ce29cedd686540b379877b8b10ab74f2bb..6e5f59010e557658ed4ebcacf0a6ae6bc0f7fdf9 100644 (file)
@@ -1,4 +1,21 @@
+%% commento segato dal lexer
+
+(* commento che va nell'ast, ma non viene contato
+    come step perche' non e' un executable
+*)
+
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 theorem a:0=0.
-reflexivity.
\ No newline at end of file
+
+%% commento segato dal lexer
+(* nota *)
+
+%% questo lo si vuole tenere anche dopo la hint
+hint. 
+
+(* commenti che non devono essere colorati perche'
+   non c'e' nulla di eseguibile dopo di loro
+*)
+
+%% EOF
index cb3aa3fb2df53fe2c7462c9a696e8def64a06bd8..82432b7c686a67b3930126aa24ee0bcc41d28324 100644 (file)
@@ -1,4 +1,16 @@
-instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
-instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
-instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.
-instance \lambda A:Set.\lambda f:A \to A \to A. \forall x,y:A. f x y = f  y x.
\ No newline at end of file
+whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
+whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
+whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.
+whelp instance \lambda A:Set.\lambda f:A \to A \to A. \forall x,y:A. f x y = f  y x.
+whelp instance \lambda A:Set.\lambda r : A \to A \to Prop. \forall x,y,z:A. r x y \to r y z \to r x z.
+
+
+λA:Set.λR:A\to A\to Prop.∀x:A.∀y:A.(R x y)\to ∀z:A.(R x z)\to ∃u:A.(R y u)∧(R z u)
+
+\lambda A:Set. \lambda R:A\to A\to Prop.\forall x:A. \forall y:A.(R x y)\to \forall z:A.(R x z)\to \exists u:A.(R y u) \land (R z u)
+
+\lambda A:Set. \lambda R:A\to A\to Prop. confluence A R.
+
+\lambda A:Set. \lambda f:A\to A\to A. \lambda g:A\to A\to A.  \forall x,y,z : A . f x (g y z) = g (f x y ) (f x z).
+  
+