snapshot

diff --git a/helm/matita/.depend b/helm/matita/.depend
index 65c9fb8f335456fe2ebb7e69ec071320a6c32bc3..9c279be545c1fcaf21ebd16f64eef6154be32edc 100644 (file)
--- a/helm/matita/.depend
+++ b/helm/matita/.depend
@@ -1,7 +1,9 @@
 matitaCicMisc.cmo: matitaTypes.cmo 
 matitaCicMisc.cmx: matitaTypes.cmx 
-matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaConsole.cmi 
-matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaConsole.cmi 
+matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaTypes.cmo \
+    matitaConsole.cmi 
+matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaTypes.cmx \
+    matitaConsole.cmi 
 matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi 
 matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi 
 matitaGeneratedGui.cmo: matitaGeneratedGui.cmi 
@@ -12,22 +14,22 @@ matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \
     matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi 
 matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \
     matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi 
-matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \
-    matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi 
-matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \
-    matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi 
+matitaInterpreter.cmo: matitaConsole.cmi matitaGui.cmi matitaMathView.cmi \
+    matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi 
+matitaInterpreter.cmx: matitaConsole.cmx matitaGui.cmx matitaMathView.cmx \
+    matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi 
 matitaMathView.cmo: matitaCicMisc.cmo matitaGui.cmi matitaTypes.cmo \
     matitaMathView.cmi 
 matitaMathView.cmx: matitaCicMisc.cmx matitaGui.cmx matitaTypes.cmx \
     matitaMathView.cmi 
-matitaMisc.cmo: matitaMisc.cmi 
-matitaMisc.cmx: matitaMisc.cmi 
+matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi 
+matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi 
 matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \
     matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaMisc.cmi \
-    matitaProof.cmi matitaTypes.cmo 
+    matitaTypes.cmo 
 matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \
     matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaMisc.cmx \
-    matitaProof.cmx matitaTypes.cmx 
+    matitaTypes.cmx 
 matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \
     matitaProof.cmi 
 matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 291507c9b4fe0c5364ed618e3afae640ea3d5e78..6420b2aa514ad4e4cd7e1d44d752146d84cbf93b 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -51,7 +51,7 @@
                          <property name="use_underline">True</property>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image164">
+                           <widget class="GtkImage" id="image174">
                              <property name="visible">True</property>
                              <property name="stock">gtk-new</property>
                              <property name="icon_size">1</property>
@@ -94,7 +94,7 @@
                          <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image165">
+                           <widget class="GtkImage" id="image175">
                              <property name="visible">True</property>
                              <property name="stock">gtk-open</property>
                              <property name="icon_size">1</property>
@@ -115,7 +115,7 @@
                          <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image166">
+                           <widget class="GtkImage" id="image176">
                              <property name="visible">True</property>
                              <property name="stock">gtk-save</property>
                              <property name="icon_size">1</property>
@@ -135,7 +135,7 @@
                          <property name="use_underline">True</property>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image167">
+                           <widget class="GtkImage" id="image177">
                              <property name="visible">True</property>
                              <property name="stock">gtk-save-as</property>
                              <property name="icon_size">1</property>
@@ -162,7 +162,7 @@
                          <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image168">
+                           <widget class="GtkImage" id="image178">
                              <property name="visible">True</property>
                              <property name="stock">gtk-quit</property>
                              <property name="icon_size">1</property>
@@ -244,7 +244,7 @@
                      <child>
                        <widget class="GtkMenuItem" id="ShowConsoleMenuItem">
                          <property name="visible">True</property>
-                         <property name="label" translatable="yes">Show console</property>
+                         <property name="label" translatable="yes">Toggle console</property>
                          <property name="use_underline">True</property>
                          <accelerator key="x" modifiers="GDK_MOD1_MASK" signal="activate"/>
                        </widget>
@@ -330,7 +330,7 @@
                  <property name="above_child">False</property>
 
                  <child>
-                   <widget class="GtkHBox" id="hbox4">
+                   <widget class="GtkHBox" id="ConsoleHBox">
                      <property name="visible">True</property>
                      <property name="homogeneous">False</property>
                      <property name="spacing">0</property>
@@ -378,7 +378,7 @@
                      <child>
                        <widget class="GtkScrolledWindow" id="ScrolledConsole">
                          <property name="visible">True</property>
-                         <property name="hscrollbar_policy">GTK_POLICY_NEVER</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>
@@ -398,7 +398,7 @@
                </widget>
                <packing>
                  <property name="shrink">True</property>
-                 <property name="resize">True</property>
+                 <property name="resize">False</property>
                </packing>
              </child>
            </widget>
@@ -900,6 +900,99 @@
            </packing>
          </child>
 
+         <child>
+           <widget class="GtkToolbar" id="toolbar8">
+             <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">50</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>
+
+             <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">50</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>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
+         </child>
+
          <child>
            <widget class="GtkToolbar" id="toolbar6">
              <property name="visible">True</property>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fad12b563772db8166e0c850c46fae22402211b2..7c9502bd414cc89b674d00a1d216a77baf8b4610 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -115,7 +115,8 @@ let proof_handler =
 
 let interpreter =
   let console = gui#console in
-  new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
+  new MatitaInterpreter.interpreter
+    ~disambiguator ~proof_handler ~console ~dbd ()
 
 (** {2 Script window handling} *)
 
@@ -137,8 +138,7 @@ let script_jump _ =
   let rec parse offset =
     if offset < len then begin
       if
-        interpreter#evalPhrase ~transparent:true
-          (String.sub raw_text offset (len - offset));
+        interpreter#evalPhrase (String.sub raw_text offset (len - offset))
       then begin
         let new_offset = interpreter#endOffset + offset in
         gui#lockScript (new_offset + locked_iter#offset);
@@ -164,8 +164,9 @@ let _ =
   gui#setQuitCallback quit;
   gui#setPhraseCallback interpreter#evalPhrase;
   gui#main#debugMenu#misc#hide ();
-  ignore (gui#main#newProofMenuItem#connect#activate
-    (gui#console#show ~msg:"theorem "));
+  ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+    gui#console#clear ();
+    gui#console#show ~msg:"theorem " ()));
   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
     match gui#chooseFile () with
     | None -> ()
@@ -198,6 +199,9 @@ let _ =
   connect_button tbar#reflexivityButton (tac A.Reflexivity);
   connect_button tbar#symmetryButton (tac A.Symmetry);
   connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
+
+(*   connect_button tbar#simplifyButton FINQUI; *)
+
   connect_button tbar#assumptionButton (tac A.Assumption);
   connect_button tbar#cutButton (tac_w_term (A.Cut hole));
   connect_button tbar#autoButton (tac A.Auto)
@@ -218,8 +222,11 @@ let _ =
         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
     addDebugItem "dump proof status to stdout" (fun _ ->
       print_endline ((get_proof ())#toString));
-    addDebugItem "hide console" gui#console#hide;
-    addDebugItem "show console" gui#console#show;
+    addDebugItem "print selected terms" (fun () ->
+      let i = ref 0 in
+      List.iter
+        (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
+        sequent_viewer#get_selected_terms)
   end
 
   (** </DEBUGGING> *)

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 810914393549a720125bcfab14c8d51ab0e024d0..222055e6539a59b8b9ecfed8bf3434d746bcb936 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -70,6 +70,7 @@ class console
   ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
   ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
 =
+  let console_height = 100 in (* pixels *)
   object (self)
     inherit GText.view obj
 
@@ -143,10 +144,12 @@ class console
       history#add (* do not push trailing phrase separator *)
         (String.sub phrase 0
           (String.length phrase - String.length _phrase_sep));
-      if _callback phrase then
-        self#hide ()
+      if _callback phrase then begin
+        self#hide ();
+        self#clear ()
         (* else callback encountered troubles, don't hide console which
         probably contains error message *)
+      end
 
     method clear () =
       let buf = self#buffer in
@@ -183,13 +186,25 @@ class console
       self#ignore_insert_text_signal false;
       self#lock
 
+    method private get_paned_prop s =
+      Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int }
+        paned#as_widget
+    method private get_position = self#get_paned_prop "position"
+    method private get_min_position = self#get_paned_prop "min-position"
+    method private get_max_position = self#get_paned_prop "max-position"
+
     method show ?(msg = "") () =
       self#buffer#insert msg;
-      paned#set_position handle_position;
+      paned#set_position (self#get_max_position - console_height);
       self#misc#grab_focus ()
     method hide () =
-      self#clear ();
-      paned#set_position max_int
+      paned#set_position self#get_max_position
+    method toggle () =
+      let pos = self#get_position in
+      if pos > self#get_max_position - console_height then
+        self#show ()
+      else
+        self#hide ()
 
       (** navigation methods: history, cursor motion, ... *)
 
@@ -198,12 +213,18 @@ class console
     method private next_phrase =
       try self#set_phrase history#next with History_failure -> ()
 
-    method wrap_exn f =
+    method wrap_exn (f: unit -> unit) =
       try
-        f ()
-      with exn ->
-        self#echo_error (sprintf "Uncaught exception: %s"
-          (Printexc.to_string exn))
+        f ();
+        true
+      with
+      | StatefulProofEngine.Tactic_failure exn ->
+          self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
+          false
+      | exn ->
+          self#echo_error (sprintf "Uncaught exception: %s"
+            (Printexc.to_string exn));
+          false
 
   end
 

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index d591e25e2e43e1c3bad9d43beeacaedbe5924801..a8e272e227d0826cc4db167a344e9ee4abc0fbbb 100644 (file)
--- a/helm/matita/matitaConsole.mli
+++ b/helm/matita/matitaConsole.mli
@@ -42,7 +42,7 @@ class console:
       * just after it; defaults to the empty string *)
     method show           : ?msg:string -> unit -> unit
     method hide           : unit -> unit
-(*     method toggle         : unit -> unit *)
+    method toggle         : unit -> unit
 
     method prompt         : string
     method set_prompt     : string -> unit
@@ -56,8 +56,9 @@ class console:
     method ignore_insert_text_signal: bool -> unit
 
       (** execute a unit -> unit function, if it raises exceptions shows them as
-      * errors in the console *)
-    method wrap_exn       : (unit -> unit) -> unit
+      * errors in the console.
+      * @return true if no exception has been raised, false otherwise *)
+    method wrap_exn       : (unit -> unit) -> bool
   end
 
   (** @param prompt user prompt (default "# ")

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index afbf9e28873379c9829cb5446894511e558a05ef..883cb634ee5a30fe6fc2d232bf6c1ebc999b6071 100644 (file)
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -36,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
     method newMenu = newMenu
-    val image164 =
+    val image174 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image164" ~info:"GtkImage" xmldata))
-    method image164 = image164
+        (Glade.get_widget_msg ~name:"image174" ~info:"GtkImage" xmldata))
+    method image174 = image174
     val newMenu_menu =
       new GMenu.menu (GtkMenu.Menu.cast
         (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
@@ -56,26 +56,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method openMenuItem = openMenuItem
-    val image165 =
+    val image175 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image165" ~info:"GtkImage" xmldata))
-    method image165 = image165
+        (Glade.get_widget_msg ~name:"image175" ~info:"GtkImage" xmldata))
+    method image175 = image175
     val saveMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveMenuItem = saveMenuItem
-    val image166 =
+    val image176 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image166" ~info:"GtkImage" xmldata))
-    method image166 = image166
+        (Glade.get_widget_msg ~name:"image176" ~info:"GtkImage" xmldata))
+    method image176 = image176
     val saveAsMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveAsMenuItem = saveAsMenuItem
-    val image167 =
+    val image177 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image167" ~info:"GtkImage" xmldata))
-    method image167 = image167
+        (Glade.get_widget_msg ~name:"image177" ~info:"GtkImage" xmldata))
+    method image177 = image177
     val separator1 =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
@@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method quitMenuItem = quitMenuItem
-    val image168 =
+    val image178 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image168" ~info:"GtkImage" xmldata))
-    method image168 = image168
+        (Glade.get_widget_msg ~name:"image178" ~info:"GtkImage" xmldata))
+    method image178 = image178
     val editMenu =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
@@ -160,10 +160,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.event_box (GtkBin.EventBox.cast
         (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
     method consoleEventBox = consoleEventBox
-    val hbox4 =
+    val consoleHBox =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox4" ~info:"GtkHBox" xmldata))
-    method hbox4 = hbox4
+        (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata))
+    method consoleHBox = consoleHBox
     val vbox6 =
       new GPack.box (GtkPack.Box.cast
         (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
@@ -320,6 +320,22 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata))
     method transitivityButton = transitivityButton
+    val toolbar8 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata))
+    method toolbar8 = toolbar8
+    val simplifyButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata))
+    method simplifyButton = simplifyButton
+    val reduceButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata))
+    method reduceButton = reduceButton
+    val whdButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata))
+    method whdButton = whdButton
     val toolbar6 =
       new GButton.toolbar (GtkButton.Toolbar.cast
         (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata))

diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli
index a85860cfbf784a5cd95b420e88746ca2ac13e653..74b2adfd0f11e0e3e85933b3edd3d822434cef40 100644 (file)
--- a/helm/matita/matitaGeneratedGui.mli
+++ b/helm/matita/matitaGeneratedGui.mli
@@ -6,21 +6,21 @@ class mainWin :
   object
     val aboutMenuItem : GMenu.menu_item
     val consoleEventBox : GBin.event_box
+    val consoleHBox : GPack.box
     val debugMenu : GMenu.menu_item
     val debugMenu_menu : GMenu.menu
     val editMenu : GMenu.menu_item
     val fileMenu : GMenu.menu_item
     val fileMenu_menu : GMenu.menu
-    val hbox4 : GPack.box
     val helpMenu : GMenu.menu_item
     val helpMenu_menu : GMenu.menu
     val hideConsoleButton : GButton.button
-    val image164 : GMisc.image
-    val image165 : GMisc.image
-    val image166 : GMisc.image
-    val image167 : GMisc.image
-    val image168 : GMisc.image
     val image169 : GMisc.image
+    val image174 : GMisc.image
+    val image175 : GMisc.image
+    val image176 : GMisc.image
+    val image177 : GMisc.image
+    val image178 : GMisc.image
     val mainMenuBar : GMenu.menu_shell
     val mainStatusBar : GMisc.statusbar
     val mainVPanes : GPack.paned
@@ -54,21 +54,21 @@ class mainWin :
     method bind : name:string -> callback:(unit -> unit) -> unit
     method check_widgets : unit -> unit
     method consoleEventBox : GBin.event_box
+    method consoleHBox : GPack.box
     method debugMenu : GMenu.menu_item
     method debugMenu_menu : GMenu.menu
     method editMenu : GMenu.menu_item
     method fileMenu : GMenu.menu_item
     method fileMenu_menu : GMenu.menu
-    method hbox4 : GPack.box
     method helpMenu : GMenu.menu_item
     method helpMenu_menu : GMenu.menu
     method hideConsoleButton : GButton.button
-    method image164 : GMisc.image
-    method image165 : GMisc.image
-    method image166 : GMisc.image
-    method image167 : GMisc.image
-    method image168 : GMisc.image
     method image169 : GMisc.image
+    method image174 : GMisc.image
+    method image175 : GMisc.image
+    method image176 : GMisc.image
+    method image177 : GMisc.image
+    method image178 : GMisc.image
     method mainMenuBar : GMenu.menu_shell
     method mainStatusBar : GMisc.statusbar
     method mainVPanes : GPack.paned
@@ -155,9 +155,11 @@ class toolBarWin :
     val existsButton : GButton.button
     val introsButton : GButton.button
     val leftButton : GButton.button
+    val reduceButton : GButton.button
     val reflexivityButton : GButton.button
     val replaceButton : GButton.button
     val rightButton : GButton.button
+    val simplifyButton : GButton.button
     val splitButton : GButton.button
     val symmetryButton : GButton.button
     val toolBarEventBox : GBin.event_box
@@ -169,8 +171,10 @@ class toolBarWin :
     val toolbar5 : GButton.toolbar
     val toolbar6 : GButton.toolbar
     val toolbar7 : GButton.toolbar
+    val toolbar8 : GButton.toolbar
     val toplevel : GWindow.window
     val transitivityButton : GButton.button
+    val whdButton : GButton.button
     val xml : Glade.glade_xml Gtk.obj
     method applyButton : GButton.button
     method assumptionButton : GButton.button
@@ -184,10 +188,12 @@ class toolBarWin :
     method existsButton : GButton.button
     method introsButton : GButton.button
     method leftButton : GButton.button
+    method reduceButton : GButton.button
     method reflexivityButton : GButton.button
     method reparent : GObj.widget -> unit
     method replaceButton : GButton.button
     method rightButton : GButton.button
+    method simplifyButton : GButton.button
     method splitButton : GButton.button
     method symmetryButton : GButton.button
     method toolBarEventBox : GBin.event_box
@@ -199,8 +205,10 @@ class toolBarWin :
     method toolbar5 : GButton.toolbar
     method toolbar6 : GButton.toolbar
     method toolbar7 : GButton.toolbar
+    method toolbar8 : GButton.toolbar
     method toplevel : GWindow.window
     method transitivityButton : GButton.button
+    method whdButton : GButton.button
     method xml : Glade.glade_xml Gtk.obj
   end
 class confirmationDialog :

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 0d46bfcfaf621f44fde9f30e9c0650d906f672f3..26cf9df086cacdd54511d0ded7bb5dab02fa40b0 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -89,7 +89,7 @@ class gui file =
             toggle_win ~check:main#showCheckMenuItem check#checkWin;
           GdkKeysyms._F5,
             toggle_win ~check:main#showScriptMenuItem script#scriptWin;
-          GdkKeysyms._x, (fun () -> console#show ());
+          GdkKeysyms._x, (fun () -> console#toggle ());
         ];
         (* about win *)
       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
@@ -123,7 +123,7 @@ class gui file =
       List.iter (fun w -> w#misc#set_sensitive false)
         [ main#saveMenuItem; main#saveAsMenuItem ];
       main#helpMenu#set_right_justified true;
-      ignore (main#showConsoleMenuItem#connect#activate console#show);
+      ignore (main#showConsoleMenuItem#connect#activate console#toggle);
         (* main *)
       connect_button main#hideConsoleButton console#hide;
 (*

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 3a4295f4ac99f94f8d75eca3ff94953f22d8b4ba..5933f6227124a6f3709d3c90e5d7b0e551747c1e 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -219,6 +219,7 @@ class proofState
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let disambiguate ast =
@@ -251,6 +252,7 @@ class proofState
     | 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
@@ -318,23 +320,14 @@ class interpreter
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let commandState =
     new commandState ~disambiguator ~proof_handler ~console ()
   in
-  let proofState = new proofState ~disambiguator ~proof_handler ~console () in
-  let wrap_exn transparent f =
-    try
-      f ();
-      true
-    with exn ->
-      if transparent then
-        raise exn
-      else
-        console#echo_error (sprintf "Uncaught exception: %s"
-          (Printexc.to_string exn));
-      false
+  let proofState =
+    new proofState ~disambiguator ~proof_handler ~console ~dbd ()
   in
   object (self)
     val mutable state = commandState
@@ -348,11 +341,18 @@ class interpreter
       | Some `Proof -> state <- proofState
       | None -> ()
 
-    method evalPhrase ?(transparent = false) s =
-      wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s))
-
-    method evalAst ?(transparent = false) s =
-      wrap_exn transparent (fun () -> self#updateState (state#evalAst s))
-
+    method evalPhrase s =
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalPhrase s))
+      in
+      if success then console#clear ();
+      success
+
+    method evalAst ast =
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalAst ast))
+      in
+      if success then console#clear ();
+      success
   end
 

diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli
index 1e4b7f7a9d0d9d5eab8aa336b0bb2ecf8273c35c..0baa4f0f1f2880931b97c20cc32c67de8bc0395d 100644 (file)
--- a/helm/matita/matitaInterpreter.mli
+++ b/helm/matita/matitaInterpreter.mli
@@ -29,6 +29,7 @@ class interpreter:
   disambiguator:MatitaTypes.disambiguator ->
   proof_handler:MatitaTypes.proof_handler ->
   console:MatitaConsole.console ->
+  dbd:Mysql.dbd ->
   unit ->
     MatitaTypes.interpreter
 

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index cdbc51e41f98488bb1c20a4081be158ec3d3e782..bb62f51c98d334818e64eb013b6300e0ca783e3e 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -236,7 +236,9 @@ class sequents_viewer ~(notebook:GPack.notebook)
     method private render_page ~page ~goal =
       sequent_viewer#load_sequent _metasenv goal;
       try
-        List.assoc goal goal2win ()
+        List.assoc goal goal2win ();
+        debug_print "set_selection none";
+        sequent_viewer#set_selection None
       with Not_found -> assert false
 
     method goto_sequent goal =
@@ -246,7 +248,7 @@ class sequents_viewer ~(notebook:GPack.notebook)
         with Not_found -> assert false
       in
       notebook#goto_page page;
-      self#render_page page goal
+      self#render_page page goal;
 
   end
 

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 9ae5cc7a98f568c978129682e1380a25e8b8b992..e9657d191155a8ebb7eddee59dea065ef7e79b1c 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -130,14 +130,13 @@ class type interpreter =
 
       (** parse a single phrase contained in the input string. Additional
       * garbage at the end of the phrase is ignored
-      * @param transparent per default the interpreter catch all exceptions ans
-      * prints them in the console. When transparent is set to true exceptions
-      * are flow through. Defaults to false
-      * @return success value of the interpretation
+      * @return true if no exception has been raised by the evaluation, false
+      * otherwise
       *)
-    method evalPhrase: ?transparent:bool -> string -> bool
+    method evalPhrase: string -> bool
 
-    method evalAst: ?transparent:bool -> DisambiguateTypes.tactical -> bool
+      (** as above, evaluating a command/tactics AST *)
+    method evalAst: DisambiguateTypes.tactical -> bool
 
       (** offset from the starting of the last string parser by evalPhrase where
       * parsing stop.