Removed a unused and troublesome feature in CoqIDE that handled shortcuts the old way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15244 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 36 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 78f98e889..afa8ea71c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -65,7 +65,6 @@ object
   method backtrack_to : GText.iter -> unit
   method backtrack_to_no_lock : GText.iter -> unit
   method clear_message : unit
-  method disconnected_keypress_handler : GdkEvent.Key.t -> bool
   method find_phrase_starting_at :
     GText.iter -> (GText.iter * GText.iter) option
   method get_insert : GText.iter
@@ -1240,43 +1239,17 @@ object(self)
              ("progress "^p^".\n") (p^".\n")) l)
 
   method active_keypress_handler k =
-    let state = GdkEvent.Key.state k in
+(*     let state = GdkEvent.Key.state k in *)
     begin
-      match  state with
-        | l when List.mem `MOD1 l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Return=k
-          then ignore(
-            if (input_buffer#insert_interactive "\n") then
-              begin
-                let i= self#get_insert#backward_word_start in
-                prerr_endline "active_kp_hf: Placing cursor";
-                self#process_until_iter_or_error i
-              end);
+      if GdkEvent.Key.keyval k = GdkKeysyms._Tab then
+        begin
+          prerr_endline "active_kp_handler for Tab";
+          self#indent_current_line;
           true
-        | l when List.mem `CONTROL l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Break=k
-          then break ();
-          false
-        | l ->
-          if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
-            prerr_endline "active_kp_handler for Tab";
-            self#indent_current_line;
-            true
-          end else false
-    end
-
-
-  method disconnected_keypress_handler k =
-    match GdkEvent.Key.state k with
-      | l when List.mem `CONTROL l ->
-        let k = GdkEvent.Key.keyval k in
-        if GdkKeysyms._c=k
-        then break ();
+        end
+      else
         false
-      | l -> false
-
+    end
 
   val mutable deact_id = None
   val mutable act_id = None
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 6bdc4585c..edefd49e2 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -118,7 +118,6 @@ class finder (view : GText.view) =
         match found with
         | None -> ()
         | Some (start, stop) ->
-          let () = Printf.printf "%i-%i\n%!" start#offset stop#offset in
           let start_mark = view#buffer#create_mark start in
           let stop_mark = view#buffer#create_mark ~left_gravity:false stop in
           let _ = view#buffer#delete_interactive ~start ~stop () in