[anjuta] sourceview: Don't block F7 shortcut (bgo#611204)

[Johannes Schmid <jhs src gnome org>]

commit 8547ae513f782fb1937c9cf0284124cc60cbb1a0
Author: Johannes Schmid <jhs idefix localdomain>
Date:   Tue Mar 2 09:13:44 2010 +0100

    sourceview: Don't block F7 shortcut (bgo#611204)

 plugins/sourceview/anjuta-view.c |   14 ++++++++++----
 1 files changed, 10 insertions(+), 4 deletions(-)
---
diff --git a/plugins/sourceview/anjuta-view.c b/plugins/sourceview/anjuta-view.c
index a5d7f4f..9a32015 100644
--- a/plugins/sourceview/anjuta-view.c
+++ b/plugins/sourceview/anjuta-view.c
@@ -676,8 +676,6 @@ anjuta_view_key_press_event		(GtkWidget *widget, GdkEventKey       *event)
 	buffer  = gtk_text_view_get_buffer (GTK_TEXT_VIEW (view));
 	
 	assist_tip = view->priv->sv->priv->assist_tip;
-	if (assist_tip)
-	{
     switch (event->keyval)
     {
       case GDK_Escape:
@@ -685,9 +683,17 @@ anjuta_view_key_press_event		(GtkWidget *widget, GdkEventKey       *event)
       case GDK_Down:
       case GDK_Page_Up:
       case GDK_Page_Down:
-        gtk_widget_destroy (GTK_WIDGET(assist_tip));
-        break;
+		if (assist_tip)
+		{
+	        gtk_widget_destroy (GTK_WIDGET(assist_tip));
+	        break;
 		}
+	  break;
+	  case GDK_F7:
+	  	/* F7 is used to toggle cursor visibility but we rather like to
+	  	 * use it as shortcut for building (#611204)
+	  	 */
+	  	return FALSE;
 	}
 	return (* GTK_WIDGET_CLASS (anjuta_view_parent_class)->key_press_event)(widget, event);
 }