snapshot, notably:

- refactoring of modules and classes: added a lot more of constructors
  and singleton instances so that objects that are really singleton
  (e.g. disambiguator, parser, db handle, ...) are not passed between
  functions
  Note that objects that are dependent on whether we are running matita
  or matitac (like the console) can't be made singleton

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index fd460dd24b1161771c6ecb19a0d050efa2fe7649..728a871120742d9617cc94fa147563cad8615e96 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -413,44 +413,6 @@
   </child>
 </widget>
 
-<widget class="GtkWindow" id="ProofWin">
-  <property name="title" translatable="yes">Matita: current proof</property>
-  <property name="type">GTK_WINDOW_TOPLEVEL</property>
-  <property name="window_position">GTK_WIN_POS_NONE</property>
-  <property name="modal">False</property>
-  <property name="default_width">700</property>
-  <property name="default_height">525</property>
-  <property name="resizable">True</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_NORMAL</property>
-  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
-
-  <child>
-    <widget class="GtkEventBox" id="ProofWinEventBox">
-      <property name="visible">True</property>
-      <property name="visible_window">True</property>
-      <property name="above_child">False</property>
-
-      <child>
-       <widget class="GtkScrolledWindow" id="ScrolledProof">
-         <property name="visible">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>
-           <placeholder/>
-         </child>
-       </widget>
-      </child>
-    </widget>
-  </child>
-</widget>
-
 <widget class="GtkFileSelection" id="FileSelectionWin">
   <property name="border_width">10</property>
   <property name="title" translatable="yes">Select File</property>
@@ -1821,45 +1783,6 @@ Copyright (C) 2004,
   </child>
 </widget>
 
-<widget class="GtkWindow" id="CheckWin">
-  <property name="width_request">300</property>
-  <property name="height_request">200</property>
-  <property name="title" translatable="yes">Matita: check term</property>
-  <property name="type">GTK_WINDOW_TOPLEVEL</property>
-  <property name="window_position">GTK_WIN_POS_NONE</property>
-  <property name="modal">False</property>
-  <property name="resizable">True</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_NORMAL</property>
-  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
-
-  <child>
-    <widget class="GtkEventBox" id="CheckWinEventBox">
-      <property name="visible">True</property>
-      <property name="visible_window">True</property>
-      <property name="above_child">False</property>
-
-      <child>
-       <widget class="GtkScrolledWindow" id="ScrolledCheck">
-         <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>
-           <placeholder/>
-         </child>
-       </widget>
-      </child>
-    </widget>
-  </child>
-</widget>
-
 <widget class="GtkWindow" id="ScriptWin">
   <property name="title" translatable="yes">Matita: script</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
@@ -1882,140 +1805,177 @@ Copyright (C) 2004,
       <property name="above_child">False</property>
 
       <child>
-       <widget class="GtkNotebook" id="scriptNotebook">
+       <widget class="GtkVBox" id="vbox7">
          <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_BOTTOM</property>
-         <property name="scrollable">False</property>
-         <property name="enable_popup">False</property>
+         <property name="homogeneous">False</property>
+         <property name="spacing">0</property>
 
          <child>
-           <widget class="GtkVBox" id="vbox4">
+           <widget class="GtkHandleBox" id="handlebox2">
              <property name="visible">True</property>
-             <property name="homogeneous">False</property>
-             <property name="spacing">0</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="toolbar1">
+               <widget class="GtkHBox" id="hbox8">
                  <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="homogeneous">False</property>
+                 <property name="spacing">0</property>
 
                  <child>
-                   <widget class="GtkToolItem" id="toolitem1">
+                   <widget class="GtkButton" id="ScriptWinTopButton">
                      <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="tooltip" translatable="yes">restart</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkButton" id="ScriptWinBackButton">
+                       <widget class="GtkImage" id="image235">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">go back 1 phrase</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NORMAL</property>
-                         <property name="focus_on_click">True</property>
-
-                         <child>
-                           <widget class="GtkImage" id="image133">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-go-back</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
+                         <property name="stock">gtk-goto-top</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
                        </widget>
                      </child>
                    </widget>
                    <packing>
+                     <property name="padding">0</property>
                      <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
+                     <property name="fill">False</property>
                    </packing>
                  </child>
 
                  <child>
-                   <widget class="GtkToolItem" id="toolitem2">
+                   <widget class="GtkButton" id="ScriptWinBackButton">
                      <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="tooltip" translatable="yes">go back 1 phrase</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkButton" id="ScriptWinJumpButton">
+                       <widget class="GtkImage" id="image133">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">execute til cursor</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NORMAL</property>
-                         <property name="focus_on_click">True</property>
+                         <property name="stock">gtk-undo</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </widget>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
-                         <child>
-                           <widget class="GtkImage" id="image134">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-jump-to</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
+                 <child>
+                   <widget class="GtkButton" id="ScriptWinJumpButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">execute until point</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image134">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-jump-to</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
                        </widget>
                      </child>
                    </widget>
                    <packing>
+                     <property name="padding">0</property>
                      <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
+                     <property name="fill">False</property>
                    </packing>
                  </child>
 
                  <child>
-                   <widget class="GtkToolItem" id="toolitem3">
+                   <widget class="GtkButton" id="ScriptWinForwardButton">
                      <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="tooltip" translatable="yes">go forward 1 phrase</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkButton" id="ScriptWinForwardButton">
+                       <widget class="GtkImage" id="image135">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">go forward 1 phrase</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NORMAL</property>
-                         <property name="focus_on_click">True</property>
+                         <property name="stock">gtk-redo</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </widget>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
-                         <child>
-                           <widget class="GtkImage" id="image135">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-go-forward</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
+                 <child>
+                   <widget class="GtkButton" id="ScriptWinBottomButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">execute all</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image236">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-goto-bottom</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
                        </widget>
                      </child>
                    </widget>
                    <packing>
+                     <property name="padding">0</property>
                      <property name="expand">False</property>
-                     <property name="homogeneous">False</property>
+                     <property name="fill">False</property>
                    </packing>
                  </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>
+
+         <child>
+           <widget class="GtkNotebook" id="ScriptNotebook">
+             <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_BOTTOM</property>
+             <property name="scrollable">False</property>
+             <property name="enable_popup">False</property>
 
              <child>
                <widget class="GtkScrolledWindow" id="ScrolledScript">
@@ -2047,79 +2007,79 @@ Copyright (C) 2004,
                  </child>
                </widget>
                <packing>
-                 <property name="padding">0</property>
-                 <property name="expand">True</property>
-                 <property name="fill">True</property>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
                </packing>
              </child>
-           </widget>
-           <packing>
-             <property name="tab_expand">False</property>
-             <property name="tab_fill">True</property>
-           </packing>
-         </child>
 
-         <child>
-           <widget class="GtkLabel" id="label7">
-             <property name="visible">True</property>
-             <property name="label" translatable="yes">script</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="scrolledwindow3">
-             <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="shadow_type">GTK_SHADOW_IN</property>
-             <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+             <child>
+               <widget class="GtkLabel" id="label7">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">script</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="GtkTreeView" id="treeview1">
+               <widget class="GtkScrolledWindow" id="ScrolledOutline">
                  <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>
+                 <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+                 <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+                 <property name="shadow_type">GTK_SHADOW_IN</property>
+                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                 <child>
+                   <widget class="GtkTreeView" id="treeview1">
+                     <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>
-           </widget>
-           <packing>
-             <property name="tab_expand">False</property>
-             <property name="tab_fill">True</property>
-           </packing>
-         </child>
 
-         <child>
-           <widget class="GtkLabel" id="label8">
-             <property name="visible">True</property>
-             <property name="label" translatable="yes">outline</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>
+             <child>
+               <widget class="GtkLabel" id="label8">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">outline</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>
            <packing>
-             <property name="type">tab</property>
+             <property name="padding">0</property>
+             <property name="expand">True</property>
+             <property name="fill">True</property>
            </packing>
          </child>
        </widget>
@@ -2276,228 +2236,243 @@ Copyright (C) 2004,
          <property name="spacing">0</property>
 
          <child>
-           <widget class="GtkHBox" id="hbox7">
+           <widget class="GtkHandleBox" id="handlebox1">
              <property name="visible">True</property>
-             <property name="homogeneous">False</property>
-             <property name="spacing">0</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="GtkButton" id="BrowserNewButton">
+               <widget class="GtkHBox" id="hbox7">
                  <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <property name="focus_on_click">True</property>
+                 <property name="homogeneous">False</property>
+                 <property name="spacing">0</property>
 
                  <child>
-                   <widget class="GtkImage" id="image191">
+                   <widget class="GtkButton" id="BrowserNewButton">
                      <property name="visible">True</property>
-                     <property name="stock">gtk-new</property>
-                     <property name="icon_size">4</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xpad">0</property>
-                     <property name="ypad">0</property>
+                     <property name="tooltip" translatable="yes">new browser win</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image191">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-new</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </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="padding">0</property>
-                 <property name="expand">False</property>
-                 <property name="fill">False</property>
-               </packing>
-             </child>
-
-             <child>
-               <widget class="GtkButton" id="BrowserBackButton">
-                 <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <property name="focus_on_click">True</property>
 
                  <child>
-                   <widget class="GtkAlignment" id="alignment3">
+                   <widget class="GtkButton" id="BrowserBackButton">
                      <property name="visible">True</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xscale">0</property>
-                     <property name="yscale">0</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>
+                     <property name="tooltip" translatable="yes">history back</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkHBox" id="hbox6">
+                       <widget class="GtkAlignment" id="alignment3">
                          <property name="visible">True</property>
-                         <property name="homogeneous">False</property>
-                         <property name="spacing">2</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">0</property>
+                         <property name="yscale">0</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="GtkImage" id="image188">
+                           <widget class="GtkHBox" id="hbox6">
                              <property name="visible">True</property>
-                             <property name="stock">gtk-go-back</property>
-                             <property name="icon_size">4</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>
+                             <property name="homogeneous">False</property>
+                             <property name="spacing">2</property>
 
-                         <child>
-                           <widget class="GtkLabel" id="label10">
-                             <property name="visible">True</property>
-                             <property name="label" translatable="yes"></property>
-                             <property name="use_underline">True</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>
+                             <child>
+                               <widget class="GtkImage" id="image188">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-go-back</property>
+                                 <property name="icon_size">4</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="GtkLabel" id="label10">
+                                 <property name="visible">True</property>
+                                 <property name="label" translatable="yes"></property>
+                                 <property name="use_underline">True</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="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">False</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="padding">0</property>
-                 <property name="expand">False</property>
-                 <property name="fill">False</property>
-               </packing>
-             </child>
-
-             <child>
-               <widget class="GtkButton" id="BrowserForwardButton">
-                 <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <property name="focus_on_click">True</property>
 
                  <child>
-                   <widget class="GtkImage" id="image189">
+                   <widget class="GtkButton" id="BrowserForwardButton">
                      <property name="visible">True</property>
-                     <property name="stock">gtk-go-forward</property>
-                     <property name="icon_size">4</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xpad">0</property>
-                     <property name="ypad">0</property>
+                     <property name="tooltip" translatable="yes">history forward</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image189">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-go-forward</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </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="padding">0</property>
-                 <property name="expand">False</property>
-                 <property name="fill">False</property>
-               </packing>
-             </child>
-
-             <child>
-               <widget class="GtkButton" id="BrowserRefreshButton">
-                 <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <property name="focus_on_click">True</property>
 
                  <child>
-                   <widget class="GtkImage" id="image229">
+                   <widget class="GtkButton" id="BrowserRefreshButton">
                      <property name="visible">True</property>
-                     <property name="stock">gtk-refresh</property>
-                     <property name="icon_size">4</property>
-                     <property name="xalign">0.5</property>
-                     <property name="yalign">0.5</property>
-                     <property name="xpad">0</property>
-                     <property name="ypad">0</property>
+                     <property name="tooltip" translatable="yes">refresh</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image229">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-refresh</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </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="padding">0</property>
-                 <property name="expand">False</property>
-                 <property name="fill">False</property>
-               </packing>
-             </child>
 
-             <child>
-               <widget class="GtkButton" id="BrowserHomeButton">
-                 <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <property name="focus_on_click">True</property>
+                 <child>
+                   <widget class="GtkButton" id="BrowserHomeButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">home</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image190">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-home</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </widget>
+                     </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
                  <child>
-                   <widget class="GtkImage" id="image190">
+                   <widget class="GtkImage" id="image187">
                      <property name="visible">True</property>
-                     <property name="stock">gtk-home</property>
+                     <property name="stock">gtk-jump-to</property>
                      <property name="icon_size">4</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">True</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="GtkImage" id="image187">
-                 <property name="visible">True</property>
-                 <property name="stock">gtk-jump-to</property>
-                 <property name="icon_size">4</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">True</property>
-               </packing>
-             </child>
 
-             <child>
-               <widget class="GtkEntry" id="BrowserUri">
-                 <property name="visible">True</property>
-                 <property name="can_focus">True</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>
+                 <child>
+                   <widget class="GtkEntry" id="BrowserUri">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">cic uri</property>
+                     <property name="can_focus">True</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>
                </widget>
-               <packing>
-                 <property name="padding">0</property>
-                 <property name="expand">True</property>
-                 <property name="fill">True</property>
-               </packing>
              </child>
            </widget>
            <packing>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 6e57c2e8ffd7614eb280330a8aaa249ac2f198cd..40f2077cfccb3f8a0f8d1f4a0061cab7e859a79d 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -51,8 +51,7 @@ let disambiguator =
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
 
-let currentProof = new MatitaProof.currentProof
-
+let currentProof = MatitaProof.instance ()
 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
 let sequents_viewer =
   let set_goal goal =
@@ -83,15 +82,10 @@ let _ = (* attach observers to proof status *)
     false);
   currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
 
-let currentProof = (currentProof :> MatitaTypes.currentProof)
-let mathViewer =
-  MatitaMathView.mathViewer ~disambiguator
-    ~currentProof:(currentProof :> MatitaTypes.currentProof) ()
+let mathViewer = MatitaMathView.mathViewer ~disambiguator ()
 let interpreter =
-  let console = (gui#console :> MatitaTypes.console) in
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof)
-    ~console ~mathViewer ~dbd ()
+  let console = gui#console in
+  MatitaInterpreter.interpreter ~disambiguator ~console ~mathViewer ()
 let _ =
   let href_callback uri =
     let term = CicAst.Uri (UriManager.string_of_uri uri, None) in
@@ -159,8 +153,7 @@ let _ =
           "Don't know what to do with file: %s\nUnrecognized file format."
           f)));
   ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
-    let currentProof = (currentProof :> MatitaTypes.currentProof) in
-    ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())));
+    ignore (MatitaMathView.cicBrowser ~disambiguator ())));
   connect_button gui#script#scriptWinForwardButton script_forward;
   connect_button gui#script#scriptWinBackButton script_back;
   connect_button gui#script#scriptWinJumpButton script_jump;
@@ -226,9 +219,14 @@ let _ =
     load_script Sys.argv.(1)
   with Invalid_argument _ -> ());
 *)
-  if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin
-    ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())
-  end else begin
+  if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin (* cicbrowser *)
+    let browser = MatitaMathView.cicBrowser ~disambiguator () in
+    Helm_registry.set "matita.mode" "cicbrowser";
+    try
+      browser#loadUri Sys.argv.(1)
+    with Invalid_argument _ -> ()
+  end else begin  (* matita *)
+    Helm_registry.set "matita.mode" "matita";
     gui#main#mainWin#show ();
     gui#toolbar#toolBarWin#show ();
     gui#console#show ()

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index e6cda30240771ca2c9abc452ee6dc8676dd2ca3e..dbb80c791ab9833f3b675cc8bae22c65e5aa85e5 100644 (file)
--- a/helm/matita/matitaCicMisc.ml
+++ b/helm/matita/matitaCicMisc.ml
@@ -60,7 +60,7 @@ let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast =
   end else
     disambiguator#disambiguateTermAst ast
 
-let get_context_and_metasenv ~(currentProof:MatitaTypes.currentProof) =
+let get_context_and_metasenv ~(currentProof:#MatitaTypes.currentProof) =
   if currentProof#onGoing () then
     let proof = currentProof#proof in
     let metasenv = proof#metasenv in

diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli
index 61111aaf18a2eb01dac2c06f6fb71db5fffe33f6..3d0de435fa83961b518238a431923818a6011c65 100644 (file)
--- a/helm/matita/matitaCicMisc.mli
+++ b/helm/matita/matitaCicMisc.mli
@@ -37,12 +37,12 @@ val canonical_context: int -> (int * 'a * 'b) list -> 'a
   * metasenv as needed *)
 val disambiguate :
   disambiguator:MatitaTypes.disambiguator ->
-  currentProof:MatitaTypes.currentProof ->
+  currentProof:#MatitaTypes.currentProof ->
   DisambiguateTypes.term ->
     DisambiguateTypes.environment * Cic.metasenv * Cic.term *
     CicUniv.universe_graph
 
 val get_context_and_metasenv:
-  currentProof:MatitaTypes.currentProof ->
+  currentProof:#MatitaTypes.currentProof ->
     Cic.context * Cic.metasenv
 

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index b192fd73255abcf009031ad0f369c502ee3c3502..11d5dcb9e41a7a7590ebc188b5ee9b10fed60a6c 100644 (file)
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -185,31 +185,6 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       toplevel#destroy ()
     method check_widgets () = ()
   end
-class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"ProofWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val proofWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
-    method proofWin = proofWin
-    val proofWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"ProofWinEventBox" ~info:"GtkEventBox" xmldata))
-    method proofWinEventBox = proofWinEventBox
-    val scrolledProof =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledProof = scrolledProof
-    method reparent parent =
-      proofWinEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
 class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
   let xmldata = Glade.create ~file  ~root:"FileSelectionWin" ?domain () in
   object (self)
@@ -622,31 +597,6 @@ class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       toplevel#destroy ()
     method check_widgets () = ()
   end
-class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"CheckWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val checkWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
-    method checkWin = checkWin
-    val checkWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"CheckWinEventBox" ~info:"GtkEventBox" xmldata))
-    method checkWinEventBox = checkWinEventBox
-    val scrolledCheck =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledCheck = scrolledCheck
-    method reparent parent =
-      checkWinEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
 class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
   let xmldata = Glade.create ~file  ~root:"ScriptWin" ?domain () in
   object (self)
@@ -663,18 +613,26 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.event_box (GtkBin.EventBox.cast
         (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata))
     method scriptWinEventBox = scriptWinEventBox
-    val scriptNotebook =
-      new GPack.notebook (GtkPack.Notebook.cast
-        (Glade.get_widget_msg ~name:"scriptNotebook" ~info:"GtkNotebook" xmldata))
-    method scriptNotebook = scriptNotebook
-    val vbox4 =
+    val vbox7 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata))
-    method vbox4 = vbox4
-    val toolbar1 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata))
-    method toolbar1 = toolbar1
+        (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata))
+    method vbox7 = vbox7
+    val handlebox2 =
+      new GBin.handle_box (GtkBin.HandleBox.cast
+        (Glade.get_widget_msg ~name:"handlebox2" ~info:"GtkHandleBox" xmldata))
+    method handlebox2 = handlebox2
+    val hbox8 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"hbox8" ~info:"GtkHBox" xmldata))
+    method hbox8 = hbox8
+    val scriptWinTopButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ScriptWinTopButton" ~info:"GtkButton" xmldata))
+    method scriptWinTopButton = scriptWinTopButton
+    val image235 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image235" ~info:"GtkImage" xmldata))
+    method image235 = image235
     val scriptWinBackButton =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata))
@@ -699,6 +657,18 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMisc.image (GtkMisc.Image.cast
         (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata))
     method image135 = image135
+    val scriptWinBottomButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata))
+    method scriptWinBottomButton = scriptWinBottomButton
+    val image236 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image236" ~info:"GtkImage" xmldata))
+    method image236 = image236
+    val scriptNotebook =
+      new GPack.notebook (GtkPack.Notebook.cast
+        (Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata))
+    method scriptNotebook = scriptNotebook
     val scrolledScript =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
         (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata))
@@ -711,10 +681,10 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMisc.label (GtkMisc.Label.cast
         (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata))
     method label7 = label7
-    val scrolledwindow3 =
+    val scrolledOutline =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"scrolledwindow3" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledwindow3 = scrolledwindow3
+        (Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledOutline = scrolledOutline
     val treeview1 =
       new GTree.view (GtkTree.TreeView.cast
         (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata))
@@ -793,6 +763,10 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GPack.box (GtkPack.Box.cast
         (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
     method browserVBox = browserVBox
+    val handlebox1 =
+      new GBin.handle_box (GtkBin.HandleBox.cast
+        (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata))
+    method handlebox1 = handlebox1
     val hbox7 =
       new GPack.box (GtkPack.Box.cast
         (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
@@ -882,9 +856,6 @@ let check_all ?(show=false) () =
   let scriptWin = new scriptWin () in
   if show then scriptWin#toplevel#show ();
   scriptWin#check_widgets ();
-  let checkWin = new checkWin () in
-  if show then checkWin#toplevel#show ();
-  checkWin#check_widgets ();
   let emptyDialog = new emptyDialog () in
   if show then emptyDialog#toplevel#show ();
   emptyDialog#check_widgets ();
@@ -906,9 +877,6 @@ let check_all ?(show=false) () =
   let fileSelectionWin = new fileSelectionWin () in
   if show then fileSelectionWin#toplevel#show ();
   fileSelectionWin#check_widgets ();
-  let proofWin = new proofWin () in
-  if show then proofWin#toplevel#show ();
-  proofWin#check_widgets ();
   let mainWin = new mainWin () in
   if show then mainWin#toplevel#show ();
   mainWin#check_widgets ();

diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli
index 26b487b88366993f31ca144a4ed53cbc100a3232..8fb25564dff6bc5bd1ac8f50bf7b33a88b67250b 100644 (file)
--- a/helm/matita/matitaGeneratedGui.mli
+++ b/helm/matita/matitaGeneratedGui.mli
@@ -98,26 +98,6 @@ class mainWin :
     method viewMenu_menu : GMenu.menu
     method xml : Glade.glade_xml Gtk.obj
   end
-class proofWin :
-  ?file:string ->
-  ?domain:string ->
-  ?autoconnect:bool ->
-  unit ->
-  object
-    val proofWin : GWindow.window
-    val proofWinEventBox : GBin.event_box
-    val scrolledProof : GBin.scrolled_window
-    val toplevel : GWindow.window
-    val xml : Glade.glade_xml Gtk.obj
-    method bind : name:string -> callback:(unit -> unit) -> unit
-    method check_widgets : unit -> unit
-    method proofWin : GWindow.window
-    method proofWinEventBox : GBin.event_box
-    method reparent : GObj.widget -> unit
-    method scrolledProof : GBin.scrolled_window
-    method toplevel : GWindow.window
-    method xml : Glade.glade_xml Gtk.obj
-  end
 class fileSelectionWin :
   ?file:string ->
   ?domain:string ->
@@ -377,56 +357,45 @@ class emptyDialog :
     method toplevel : GWindow.dialog_any
     method xml : Glade.glade_xml Gtk.obj
   end
-class checkWin :
-  ?file:string ->
-  ?domain:string ->
-  ?autoconnect:bool ->
-  unit ->
-  object
-    val checkWin : GWindow.window
-    val checkWinEventBox : GBin.event_box
-    val scrolledCheck : GBin.scrolled_window
-    val toplevel : GWindow.window
-    val xml : Glade.glade_xml Gtk.obj
-    method bind : name:string -> callback:(unit -> unit) -> unit
-    method checkWin : GWindow.window
-    method checkWinEventBox : GBin.event_box
-    method check_widgets : unit -> unit
-    method reparent : GObj.widget -> unit
-    method scrolledCheck : GBin.scrolled_window
-    method toplevel : GWindow.window
-    method xml : Glade.glade_xml Gtk.obj
-  end
 class scriptWin :
   ?file:string ->
   ?domain:string ->
   ?autoconnect:bool ->
   unit ->
   object
+    val handlebox2 : GBin.handle_box
+    val hbox8 : GPack.box
     val image133 : GMisc.image
     val image134 : GMisc.image
     val image135 : GMisc.image
+    val image235 : GMisc.image
+    val image236 : GMisc.image
     val label7 : GMisc.label
     val label8 : GMisc.label
     val scriptNotebook : GPack.notebook
     val scriptTextView : GText.view
     val scriptWin : GWindow.window
     val scriptWinBackButton : GButton.button
+    val scriptWinBottomButton : GButton.button
     val scriptWinEventBox : GBin.event_box
     val scriptWinForwardButton : GButton.button
     val scriptWinJumpButton : GButton.button
+    val scriptWinTopButton : GButton.button
+    val scrolledOutline : GBin.scrolled_window
     val scrolledScript : GBin.scrolled_window
-    val scrolledwindow3 : GBin.scrolled_window
-    val toolbar1 : GButton.toolbar
     val toplevel : GWindow.window
     val treeview1 : GTree.view
-    val vbox4 : GPack.box
+    val vbox7 : GPack.box
     val xml : Glade.glade_xml Gtk.obj
     method bind : name:string -> callback:(unit -> unit) -> unit
     method check_widgets : unit -> unit
+    method handlebox2 : GBin.handle_box
+    method hbox8 : GPack.box
     method image133 : GMisc.image
     method image134 : GMisc.image
     method image135 : GMisc.image
+    method image235 : GMisc.image
+    method image236 : GMisc.image
     method label7 : GMisc.label
     method label8 : GMisc.label
     method reparent : GObj.widget -> unit
@@ -434,15 +403,16 @@ class scriptWin :
     method scriptTextView : GText.view
     method scriptWin : GWindow.window
     method scriptWinBackButton : GButton.button
+    method scriptWinBottomButton : GButton.button
     method scriptWinEventBox : GBin.event_box
     method scriptWinForwardButton : GButton.button
     method scriptWinJumpButton : GButton.button
+    method scriptWinTopButton : GButton.button
+    method scrolledOutline : GBin.scrolled_window
     method scrolledScript : GBin.scrolled_window
-    method scrolledwindow3 : GBin.scrolled_window
-    method toolbar1 : GButton.toolbar
     method toplevel : GWindow.window
     method treeview1 : GTree.view
-    method vbox4 : GPack.box
+    method vbox7 : GPack.box
     method xml : Glade.glade_xml Gtk.obj
   end
 class textDialog :
@@ -492,6 +462,7 @@ class browserWin :
     val browserWin : GWindow.window
     val browserWinEventBox : GBin.event_box
     val frame1 : GBin.frame
+    val handlebox1 : GBin.handle_box
     val hbox6 : GPack.box
     val hbox7 : GPack.box
     val image187 : GMisc.image
@@ -517,6 +488,7 @@ class browserWin :
     method browserWinEventBox : GBin.event_box
     method check_widgets : unit -> unit
     method frame1 : GBin.frame
+    method handlebox1 : GBin.handle_box
     method hbox6 : GPack.box
     method hbox7 : GPack.box
     method image187 : GMisc.image

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fef22143ad2c759aa9204950782a7456116018f6..04d52cd9e3555a0cdb7c2a1eeec498644d7fdbaa 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -35,12 +35,10 @@ class gui file =
   let main = new mainWin ~file () in
   let about = new aboutWin ~file () in
   let fileSel = new fileSelectionWin ~file () in
-  let proof = new proofWin ~file () in
-  let check = new checkWin ~file () in
   let script = new scriptWin ~file () in
   let keyBindingBoxes = (* event boxes which should receive global key events *)
-    [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox;
-      check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ]
+    [ toolbar#toolBarEventBox; main#mainWinEventBox;
+      script#scriptWinEventBox; main#consoleEventBox ]
   in
   let console =
     MatitaConsole.console ~evbox:main#consoleEventBox
@@ -62,7 +60,7 @@ class gui file =
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
         (let c w = (w :> <check_widgets: unit -> unit>) in
-         [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]);
+         [ c about; c fileSel; c main; c toolbar; c script ]);
         (* key bindings *)
       List.iter (* global key bindings *)
         (fun (key, callback) -> self#addKeyBinding key callback)
@@ -121,11 +119,9 @@ class gui file =
       console#misc#grab_focus ();
 
     method about = about
-    method check = check
     method console = console
     method fileSel = fileSel
     method main = main
-    method proof = proof
     method script = script
     method toolbar = toolbar
 

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index 1d3f1220b58aee4a6f00cbbcb96b5579db6d9ff5..acc244aa942ab0f729ed28131b9d1890c37ecc8c 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -34,10 +34,8 @@ class gui :
       (** {2 Access to singleton instances of lower-level GTK widgets} *)
 
     method about :        MatitaGeneratedGui.aboutWin
-    method check :        MatitaGeneratedGui.checkWin
     method fileSel :      MatitaGeneratedGui.fileSelectionWin
     method main :         MatitaGeneratedGui.mainWin
-    method proof :        MatitaGeneratedGui.proofWin
     method script:        MatitaGeneratedGui.scriptWin
     method toolbar :      MatitaGeneratedGui.toolBarWin
 

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 78d30c4cd062a16898dc16eff268fce257940a91..640b7406ee17f925832f864d410f7e95fb5b233c 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -64,9 +64,12 @@ class virtual interpreterState =
     (* static values, shared by all states inheriting this class *)
   let loc = ref None in
   let history = ref [] in
-  fun ~(console: MatitaTypes.console) ->
+  fun ~(console: #MatitaTypes.console) ->
   object (self)
 
+    val dbd = MatitaMisc.dbd_instance ()
+    val currentProof = MatitaProof.instance ()
+
       (** eval a toplevel phrase in the current state and return the new state
       *)
     method parsePhrase s =
@@ -103,10 +106,8 @@ class virtual interpreterState =
   (** Implements phrases that should be accepted in all states *)
 class sharedState
   ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
+  ~(console: #MatitaTypes.console)
   ?(mathViewer: MatitaTypes.mathViewer option)
-  ~(dbd: Mysql.dbd)
   ()
 =
   object (self)
@@ -307,7 +308,7 @@ let
     * - save object to disk in xml format
     * - register uri to the getter 
     * - save universe file *)
-let add_constant_to_world ~(console:MatitaTypes.console)
+let add_constant_to_world ~(console: #MatitaTypes.console)
   ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph ()
 =
   let suri = UriManager.string_of_uri uri in
@@ -324,7 +325,7 @@ let add_constant_to_world ~(console:MatitaTypes.console)
     console#echo_message (sprintf "%s constant defined" suri)
   end
 
-let add_inductive_def_to_world ~(console:MatitaTypes.console)
+let add_inductive_def_to_world ~(console: #MatitaTypes.console)
   ~dbd ~uri ~indTypes ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph ()
 =
   let suri = UriManager.string_of_uri uri in
@@ -360,15 +361,11 @@ let add_inductive_def_to_world ~(console:MatitaTypes.console)
   (** Implements phrases that should be accepted only in Command state *)
 class commandState
   ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
+  ~(console: #MatitaTypes.console)
   ?mathViewer
-  ~(dbd: Mysql.dbd)
   ()
 =
-  let shared =
-    new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+  let shared = new sharedState ~disambiguator ~console ?mathViewer () in
   object (self)
     inherit interpreterState ~console
 
@@ -519,67 +516,64 @@ let namer_of names =
   * tacticals *)
 class proofState
   ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
+  ~(console: #MatitaTypes.console)
   ?mathViewer
-  ~(dbd: Mysql.dbd)
   ()
 =
-  let disambiguate ast =
-    let (_, _, term, _) =
-      MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
-    in
-    term
-  in
-    (** tactic AST -> ProofEngineTypes.tactic *)
-  let rec lookup_tactic = function
-    | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
-    | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
-        PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-    | TacticAst.Reflexivity -> Tactics.reflexivity
-    | TacticAst.Assumption -> Tactics.assumption
-    | TacticAst.Contradiction -> Tactics.contradiction
-    | TacticAst.Exists -> Tactics.exists
-    | TacticAst.Fourier -> Tactics.fourier
-    | TacticAst.Left -> Tactics.left
-    | TacticAst.Right -> Tactics.right
-    | TacticAst.Ring -> Tactics.ring
-    | TacticAst.Split -> Tactics.split
-    | TacticAst.Symmetry -> Tactics.symmetry
-    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
-    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
-    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
-    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
-    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
-    | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
-        Tactics.elim_intros_simpl (disambiguate term)
-    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
-    | TacticAst.Replace (what, with_what) ->
-        Tactics.replace ~what:(disambiguate what)
-          ~with_what:(disambiguate with_what)
-    | TacticAst.Auto -> Tactics.auto_new ~dbd
-  (*
-    (* TODO Zack a lot more of tactics to be implemented here ... *)
-    | TacticAst.Change of 'term * 'term * 'ident option
-    | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
-    | TacticAst.Decompose of 'ident * 'ident list
-    | TacticAst.Discriminate of 'ident
-    | TacticAst.Fold of reduction_kind * 'term
-    | TacticAst.Injection of 'ident
-    | 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
-  *)
-    | _ ->
-        MatitaTypes.not_implemented "some tactic"
-  in
-  let shared =
-    new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+  let shared = new sharedState ~disambiguator ~console ?mathViewer () in
   object (self)
     inherit interpreterState ~console
 
+    method private disambiguate ast =
+      let (_, _, term, _) =
+        MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+      in
+      term
+
+    (** tactic AST -> ProofEngineTypes.tactic *)
+    method private lookup_tactic = function
+      | TacticAst.LocatedTactic (_, tactic) -> self#lookup_tactic tactic
+      | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
+          PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names)
+            ()
+      | TacticAst.Reflexivity -> Tactics.reflexivity
+      | TacticAst.Assumption -> Tactics.assumption
+      | TacticAst.Contradiction -> Tactics.contradiction
+      | TacticAst.Exists -> Tactics.exists
+      | TacticAst.Fourier -> Tactics.fourier
+      | TacticAst.Left -> Tactics.left
+      | TacticAst.Right -> Tactics.right
+      | TacticAst.Ring -> Tactics.ring
+      | TacticAst.Split -> Tactics.split
+      | TacticAst.Symmetry -> Tactics.symmetry
+      | TacticAst.Transitivity term ->
+          Tactics.transitivity (self#disambiguate term)
+      | TacticAst.Apply term -> Tactics.apply (self#disambiguate term)
+      | TacticAst.Absurd term -> Tactics.absurd (self#disambiguate term)
+      | TacticAst.Exact term -> Tactics.exact (self#disambiguate term)
+      | TacticAst.Cut term -> Tactics.cut (self#disambiguate term)
+      | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+          Tactics.elim_intros_simpl (self#disambiguate term)
+      | TacticAst.ElimType term -> Tactics.elim_type (self#disambiguate term)
+      | TacticAst.Replace (what, with_what) ->
+          Tactics.replace ~what:(self#disambiguate what)
+            ~with_what:(self#disambiguate with_what)
+      | TacticAst.Auto -> Tactics.auto_new ~dbd
+    (*
+      (* TODO Zack a lot more of tactics to be implemented here ... *)
+      | TacticAst.Change of 'term * 'term * 'ident option
+      | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+      | TacticAst.Decompose of 'ident * 'ident list
+      | TacticAst.Discriminate of 'ident
+      | TacticAst.Fold of reduction_kind * 'term
+      | TacticAst.Injection of 'ident
+      | 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
+    *)
+      | _ -> MatitaTypes.not_implemented "some tactic"
+
     method evalTactical = function
       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
       | TacticAst.Command TacticAst.Abort ->
@@ -616,7 +610,7 @@ class proofState
           List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
           New_state Proof
       | TacticAst.Tactic tactic_phrase ->
-          let tactic = lookup_tactic tactic_phrase in
+          let tactic = self#lookup_tactic tactic_phrase in
           currentProof#proof#apply_tactic tactic;
           New_state Proof
       | tactical -> shared#evalTactical tactical
@@ -624,18 +618,12 @@ class proofState
 
 class interpreter
   ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
+  ~(console: #MatitaTypes.console)
   ?mathViewer
-  ~(dbd: Mysql.dbd)
   ()
 =
-  let commandState =
-    new commandState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
-  let proofState =
-    new proofState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+  let commandState = new commandState ~disambiguator ~console ?mathViewer () in
+  let proofState = new proofState ~disambiguator ~console ?mathViewer () in
   object (self)
     val mutable state = commandState
 
@@ -661,3 +649,11 @@ class interpreter
     method evalAst ast = self#eval (fun () -> state#evalAst ast)
   end
 
+let interpreter
+  ~(disambiguator: MatitaTypes.disambiguator)
+  ~(console: #MatitaTypes.console)
+  ?mathViewer
+  ()
+=
+  new interpreter ~disambiguator ~console ?mathViewer ()
+

diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli
index 7886a564a719da068c4d72d4773e4c38095f3f95..2b0ad56da8a20f898b503d83e05f391846804b18 100644 (file)
--- a/helm/matita/matitaInterpreter.mli
+++ b/helm/matita/matitaInterpreter.mli
@@ -25,12 +25,10 @@
 
 exception Command_error of string
 
-class interpreter:
+val interpreter:
   disambiguator:MatitaTypes.disambiguator ->
-  currentProof:MatitaTypes.currentProof ->
-  console:MatitaTypes.console ->
+  console:#MatitaTypes.console ->
   ?mathViewer:MatitaTypes.mathViewer ->
-  dbd:Mysql.dbd ->
   unit ->
     MatitaTypes.interpreter
 

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7bf464a9d8390b8fea4783e6cd93220a1a4398af..626e456349752d91c84ed3d3d6f2b86df5143f9a 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -267,7 +267,6 @@ let cicBrowsers = ref []
 
 class cicBrowser 
   ~(disambiguator:MatitaTypes.disambiguator)
-  ~(currentProof:MatitaTypes.currentProof)
   ~(history:string MatitaMisc.history)
   ()
 =
@@ -286,24 +285,33 @@ class cicBrowser
     with exn ->
       fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
   in
+  let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
   object (self)
     initializer
-      ignore (win#browserUri#connect#activate (fun () ->
-        self#_loadUri win#browserUri#text));
-      ignore (win#browserHomeButton#connect#clicked (fun () ->
-        self#_loadUri current_proof_uri));
-      ignore (win#browserRefreshButton#connect#clicked self#refresh);
-      ignore (win#browserBackButton#connect#clicked self#back);
-      ignore (win#browserForwardButton#connect#clicked self#forward);
+      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
+        self#_loadUri win#browserUri#text)));
+      ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
+        self#_loadUri current_proof_uri)));
+      ignore (win#browserRefreshButton#connect#clicked
+        (handle_error' self#refresh));
+      ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
+      ignore (win#browserForwardButton#connect#clicked
+        (handle_error' self#forward));
       ignore (win#toplevel#event#connect#delete (fun _ ->
         let my_id = Oo.id self in
         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        if !cicBrowsers = [] &&
+          Helm_registry.get "matita.mode" = "cicbrowser"
+        then
+          GMain.quit ();
         false));
       mathView#set_href_callback (Some (fun uri ->
         handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri))));
       self#_loadUri ~add_to_history:false blank_uri;
       toplevel#show ();
 
+    val currentProof = MatitaProof.instance ()
+
     val mutable current_uri = ""
     val mutable current_infos = None
     val mutable current_mathml = None
@@ -418,10 +426,10 @@ let sequents_viewer ~(notebook:GPack.notebook)
 =
   new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
 
-let cicBrowser ~disambiguator ~currentProof () =
+let cicBrowser ~disambiguator () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
-    let browser = new cicBrowser ~disambiguator ~currentProof ~history () in
+    let browser = new cicBrowser ~disambiguator ~history () in
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
@@ -442,13 +450,12 @@ let cicBrowser ~disambiguator ~currentProof () =
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 
-class mathViewer ~disambiguator ~currentProof =
+class mathViewer ~disambiguator =
   object
     method checkTerm (src:MatitaTypes.term_source) =
-      let browser = cicBrowser ~disambiguator ~currentProof () in
+      let browser = cicBrowser ~disambiguator () in
       browser#loadTerm src
   end
 
-let mathViewer ~disambiguator ~currentProof () =
-  new mathViewer ~disambiguator ~currentProof
+let mathViewer ~disambiguator () = new mathViewer ~disambiguator
 

diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli
index de8edc8559621959b7b02451903cdced3a70259a..cdc9a8d65ead9e96fbb9eafadad7cea346b397ce 100644 (file)
--- a/helm/matita/matitaMathView.mli
+++ b/helm/matita/matitaMathView.mli
@@ -85,7 +85,6 @@ val sequents_viewer:
 
 val cicBrowser:
   disambiguator:MatitaTypes.disambiguator ->
-  currentProof:MatitaTypes.currentProof ->
   unit ->
     MatitaTypes.cicBrowser
 
@@ -93,7 +92,6 @@ val refresh_all_browsers: unit -> unit
 
 val mathViewer:
   disambiguator:MatitaTypes.disambiguator ->
-  currentProof:MatitaTypes.currentProof ->
   unit ->
     MatitaTypes.mathViewer
 

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c3b83fd472f31453181f1598fd786f88d24ff442..dd84abcbd00de0e7ffc32b60907f409a1158a029 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -130,3 +130,13 @@ class ['a] browser_history ?memento size init =
     method save = (Array.copy data, hd, tl, cur)
   end
 
+let dbd_instance =
+  let dbd = lazy (
+    Mysql.quick_connect
+      ~host:(Helm_registry.get "db.host")
+      ~user:(Helm_registry.get "db.user")
+      ~database:(Helm_registry.get "db.database")
+      ())
+  in
+  fun () -> Lazy.force dbd
+

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index afaa631a08f01646e773aa505301c710db2718d3..36318dc1fa0d2dbafa956c15e9336a92a902da3f 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -66,3 +66,6 @@ class shell_history : int -> [string] history
   * @param first element in history (this history is never empty) *)
 class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history
 
+  (** {2 db handling} *)
+val dbd_instance: unit -> Mysql.dbd
+

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 54ebdf6cf7663340bf5907d433a63ee3f963854c..9afb90a714b36ca53090f0e63b68aa743d2bd9f0 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -151,4 +151,7 @@ let proof ?uri ~metasenv ~typ () =
   new proof ~typ ~metasenv ~body ?uri ()
 
 let currentProof () = new currentProof
+let instance =
+  let currentProof = lazy (currentProof ()) in 
+  fun () -> Lazy.force currentProof
 

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index 566777fc1c8e3e61135127b1c1014a1e33f162e6..9ed6221917d215277b6783435b788bb4ebeb51b9 100644 (file)
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -36,7 +36,7 @@ val proof:
     MatitaTypes.proof
 
   (** current proof handler *)
-class currentProof:
+class type currentProof =
   object
     inherit MatitaTypes.currentProof
     
@@ -52,3 +52,8 @@ class currentProof:
     method connect: [`Abort|`Quit] -> (unit -> bool) -> unit
   end
 
+val currentProof: unit -> currentProof
+
+  (** currentProof singleton instance *)
+val instance: unit -> currentProof
+

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index bb796db1e79d8f005630d227cfacd8bdee3437a7..87c30cfea08001eca25930502198dcad170e4468 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -78,10 +78,7 @@ let disambiguator =
     ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
     ()
 let console = new tty_console
-let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof)
-let interpreter =
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof ~console ~dbd ()
+let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()
 
 let run_script fname =
   message (sprintf "execution of %s started:" fname);