propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 05 19:05:16 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 05 20:06:24 2013 +0100
@@ -54,7 +54,8 @@
 
 class Pretty_Text_Area(
   view: View,
-  background: Option[Color] = None) extends JEditEmbeddedTextArea
+  background: Option[Color] = None,
+  propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
 {
   text_area =>
 
@@ -167,13 +168,23 @@
         case KeyEvent.VK_C
         if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
           Registers.copy(text_area, '$')
+          evt.consume
         case KeyEvent.VK_ESCAPE =>
           Window.getWindows foreach {
             case c: Pretty_Tooltip => c.dispose
             case _ =>
           }
+          evt.consume
         case _ =>
       }
+      if (propagate_keys && !evt.isConsumed)
+        view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
+    }
+
+    override def keyTyped(evt: KeyEvent)
+    {
+      if (propagate_keys && !evt.isConsumed)
+        view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
     }
   })
 

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 05 19:05:16 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 05 20:06:24 2013 +0100
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Color, Point, BorderLayout, Window, Dimension}
-import java.awt.event.{WindowEvent, WindowAdapter}
+import java.awt.event.{WindowEvent, WindowAdapter, KeyEvent, KeyAdapter, KeyListener}
 import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent}
 import javax.swing.border.LineBorder
 
@@ -55,7 +55,7 @@
 
   /* pretty text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color))
+  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color), true)
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, results, body)