# HG changeset patch # User wenzelm # Date 1379866054 -7200 # Node ID 322a3ff42b33f56d91ea6c23f303b4dc1fd0ea99 # Parent f5e9d182f64505d874c1d0129b488ad7295f8ffd completion popup for history text field; imitate view font, for default rendering of symbols; tuned signature; diff -r f5e9d182f645 -r 322a3ff42b33 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sun Sep 22 14:30:34 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Sun Sep 22 18:07:34 2013 +0200 @@ -10,20 +10,21 @@ import isabelle._ import java.awt.{Color, Font, Point, BorderLayout, Dimension} -import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} +import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} import javax.swing.border.LineBorder import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked -import org.gjt.sp.jedit.{View, Debug} +import org.gjt.sp.jedit.View import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround} object Completion_Popup { - /* setup for jEdit text area */ + /** jEdit text area **/ object Text_Area { @@ -156,14 +157,7 @@ if (!evt.isConsumed) { dismissed() if (evt.getKeyChar != '\b') { - val mod = evt.getModifiers - val special = - // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java - (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || - (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && - !Debug.ALT_KEY_PRESSED_DISABLED || - (mod & InputEvent.META_MASK) != 0 - + val special = JEdit_Lib.special_key(evt) if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { input_delay.revoke() action(immediate = PIDE.options.bool("jedit_completion_immediate")) @@ -213,6 +207,143 @@ text_area.removeKeyListener(outer_key_listener) } } + + + + /** history text field **/ + + class History_Text_Field( + name: String = null, + instant_popups: Boolean = false, + enter_adds_to_history: Boolean = true, + syntax: Outer_Syntax = Outer_Syntax.init) extends + HistoryTextField(name, instant_popups, enter_adds_to_history) + { + text_field => + + + private var completion_popup: Option[Completion_Popup] = None + + + /* dismiss */ + + private def dismissed(): Boolean = + { + completion_popup match { + case Some(completion) => + completion.hide_popup() + completion_popup = None + true + case None => + false + } + } + + + /* insert */ + + private def insert(item: Completion.Item) + { + Swing_Thread.require() + + val len = item.original.length + if (text_field.isEditable && len > 0) { + val caret = text_field.getCaret.getDot + val content = text_field.getText + JEdit_Lib.try_get_text(content, Text.Range(caret - len, caret)) match { + case Some(text) if text == item.original => + text_field.setText( + content.substring(0, caret - len) + + item.replacement + + content.substring(caret)) + case _ => + } + } + } + + + /* completion action */ + + def action() + { + GUI.layered_pane(text_field) match { + case Some(layered) if text_field.isEditable => + val history = PIDE.completion_history.value + + val caret = text_field.getCaret.getDot + val text = text_field.getText.substring(0, caret) + + syntax.completion.complete(history, decode = true, explicit = false, text) match { + case Some(result) => + val fm = text_field.getFontMetrics(text_field.getFont) + val loc = + SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered) + val font = + text_field.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) + + val completion = new Completion_Popup(layered, loc, font, result.items) + { + override def complete(item: Completion.Item) { + PIDE.completion_history.update(item) + insert(item) + } + override def propagate(evt: KeyEvent) { + if (!evt.isConsumed) text_field.processKeyEvent(evt) + } + override def refocus() { text_field.requestFocus } + } + completion_popup = Some(completion) + completion.show_popup() + + case None => + } + case _ => + } + } + + + /* process key event */ + + private def process(evt: KeyEvent) + { + if (PIDE.options.bool("jedit_completion")) { + dismissed() + if (evt.getKeyChar != '\b') { + val special = JEdit_Lib.special_key(evt) + if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { + process_delay.revoke() + action() + } + else process_delay.invoke() + } + } + } + + private val process_delay = + Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + action() + } + + override def processKeyEvent(evt0: KeyEvent) + { + val evt = KeyEventWorkaround.processKeyEvent(evt0) + if (evt != null) { + evt.getID match { + case KeyEvent.KEY_PRESSED => + val key_code = evt.getKeyCode + if (key_code == KeyEvent.VK_ESCAPE) { + if (dismissed()) evt.consume + } + case KeyEvent.KEY_TYPED => + super.processKeyEvent(evt) + process(evt) + evt.consume + case _ => + } + if (!evt.isConsumed) super.processKeyEvent(evt) + } + } + } } diff -r f5e9d182f645 -r 322a3ff42b33 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Sun Sep 22 14:30:34 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Sun Sep 22 18:07:34 2013 +0200 @@ -18,7 +18,6 @@ import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} import org.gjt.sp.jedit.View -import org.gjt.sp.jedit.gui.HistoryTextField class Find_Dockable(view: View, position: String) extends Dockable(view, position) @@ -109,7 +108,7 @@ tooltip = "Search criteria for find operation" } - private val query = new HistoryTextField("isabelle-find-theorems") { + private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") { override def processKeyEvent(evt: KeyEvent) { if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked @@ -118,6 +117,7 @@ { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) } setColumns(40) setToolTipText(query_label.tooltip) + setFont(Token_Markup.imitate_font(Rendering.font_family(), getFont)) } private case class Context_Entry(val name: String, val description: String) diff -r f5e9d182f645 -r 322a3ff42b33 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sun Sep 22 14:30:34 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Sep 22 18:07:34 2013 +0200 @@ -10,12 +10,12 @@ import isabelle._ import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension} -import java.awt.event.{KeyEvent, KeyListener} +import java.awt.event.{InputEvent, KeyEvent, KeyListener} import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.annotation.tailrec -import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities} +import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug} import org.gjt.sp.jedit.gui.KeyEventWorkaround import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} @@ -157,6 +157,10 @@ try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } + def try_get_text(text: String, range: Text.Range): Option[String] = + try { Some(text.substring(range.start, range.stop)) } + catch { case _: IndexOutOfBoundsException => None } + /* buffer range */ @@ -336,5 +340,15 @@ def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) } } } + + def special_key(evt: KeyEvent): Boolean = + { + // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java + val mod = evt.getModifiers + (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || + (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && + !Debug.ALT_KEY_PRESSED_DISABLED || + (mod & InputEvent.META_MASK) != 0 + } } diff -r f5e9d182f645 -r 322a3ff42b33 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sun Sep 22 14:30:34 2013 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sun Sep 22 18:07:34 2013 +0200 @@ -73,13 +73,13 @@ private def font_metrics(font: Font): LineMetrics = font.getLineMetrics("", new FontRenderContext(null, false, false)) - private def imitate_font(family: String, font: Font): Font = + def imitate_font(family: String, font: Font): Font = { - val font1 = new Font (family, font.getStyle, font.getSize) + val font1 = new Font(family, font.getStyle, font.getSize) font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize) } - private def transform_font(font: Font, transform: AffineTransform): Font = + def transform_font(font: Font, transform: AffineTransform): Font = { import scala.collection.JavaConversions._ font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))