X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=3cf09934972746fd9de3692b2b188449a71f0f26;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=028a17710ed5e03399c2fc0284c4302095806d5e;hpb=0cb00e631ea54deacbfde12e1c458ca602b97870;p=helm.git diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index 028a17710..3cf099349 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -123,7 +123,8 @@ module Make(C:Disambiguate.Callbacks) = mmlwidget#thaw end else if key = GdkKeysyms._BackSpace then - Mathml_editor.drop tex_editor false ; + 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 ;