From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Jul 2003 10:30:01 +0000 (+0000)
Subject: Ctr+Backspace is now enabled. Used to perform "alternative" deletion.
X-Git-Tag: camera_ready~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=65e3c9976212e04a4678ff9ce9e3c2f436d06d33

Ctr+Backspace is now enabled. Used to perform "alternative" deletion.
---

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 ;