X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=3cf09934972746fd9de3692b2b188449a71f0f26;hb=f9fb6aea5ebbb04018ce2b9e4a395339b58d8ff9;hp=d97eb51c46addf97deff9a7d64141b724b421696;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index d97eb51c4..3cf099349 100644
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -123,9 +123,12 @@ module Make(C:Disambiguate.Callbacks) =
            mmlwidget#thaw
           end
          else if key = GdkKeysyms._BackSpace then
-          Mathml_editor.drop tex_editor false ;
-         mmlwidget#thaw ;
-         false) in
+          Mathml_editor.drop tex_editor
+           (List.mem `CONTROL (GdkEvent.Key.state e)) ;
+         let adj = mmlwidget#get_hadjustment in
+          mmlwidget#thaw ;
+          adj#set_value adj#upper ;
+          false) in
     let id_to_uris =
      match share_id_to_uris_with with
         None -> ref empty_id_to_uris