completion popup for history text field;
authorwenzelm
Sun Sep 22 18:07:34 2013 +0200 (2013-09-22 ago)
changeset 53784322a3ff42b33
parent 53783 f5e9d182f645
child 53785 e64edcc2f8bf
completion popup for history text field;
imitate view font, for default rendering of symbols;
tuned signature;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 22 14:30:34 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 22 18:07:34 2013 +0200
     1.3 @@ -10,20 +10,21 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Color, Font, Point, BorderLayout, Dimension}
     1.7 -import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.8 +import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.9  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    1.10  import javax.swing.border.LineBorder
    1.11  
    1.12  import scala.swing.{ListView, ScrollPane}
    1.13  import scala.swing.event.MouseClicked
    1.14  
    1.15 -import org.gjt.sp.jedit.{View, Debug}
    1.16 +import org.gjt.sp.jedit.View
    1.17  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.18 +import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    1.19  
    1.20  
    1.21  object Completion_Popup
    1.22  {
    1.23 -  /* setup for jEdit text area */
    1.24 +  /** jEdit text area **/
    1.25  
    1.26    object Text_Area
    1.27    {
    1.28 @@ -156,14 +157,7 @@
    1.29          if (!evt.isConsumed) {
    1.30            dismissed()
    1.31            if (evt.getKeyChar != '\b') {
    1.32 -            val mod = evt.getModifiers
    1.33 -            val special =
    1.34 -              // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    1.35 -              (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    1.36 -              (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    1.37 -                !Debug.ALT_KEY_PRESSED_DISABLED ||
    1.38 -              (mod & InputEvent.META_MASK) != 0
    1.39 -
    1.40 +            val special = JEdit_Lib.special_key(evt)
    1.41              if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    1.42                input_delay.revoke()
    1.43                action(immediate = PIDE.options.bool("jedit_completion_immediate"))
    1.44 @@ -213,6 +207,143 @@
    1.45        text_area.removeKeyListener(outer_key_listener)
    1.46      }
    1.47    }
    1.48 +
    1.49 +
    1.50 +
    1.51 +  /** history text field **/
    1.52 +
    1.53 +  class History_Text_Field(
    1.54 +    name: String = null,
    1.55 +    instant_popups: Boolean = false,
    1.56 +    enter_adds_to_history: Boolean = true,
    1.57 +    syntax: Outer_Syntax = Outer_Syntax.init) extends
    1.58 +    HistoryTextField(name, instant_popups, enter_adds_to_history)
    1.59 +  {
    1.60 +    text_field =>
    1.61 +
    1.62 +
    1.63 +    private var completion_popup: Option[Completion_Popup] = None
    1.64 +
    1.65 +
    1.66 +    /* dismiss */
    1.67 +
    1.68 +    private def dismissed(): Boolean =
    1.69 +    {
    1.70 +      completion_popup match {
    1.71 +        case Some(completion) =>
    1.72 +          completion.hide_popup()
    1.73 +          completion_popup = None
    1.74 +          true
    1.75 +        case None =>
    1.76 +          false
    1.77 +      }
    1.78 +    }
    1.79 +
    1.80 +
    1.81 +    /* insert */
    1.82 +
    1.83 +    private def insert(item: Completion.Item)
    1.84 +    {
    1.85 +      Swing_Thread.require()
    1.86 +
    1.87 +      val len = item.original.length
    1.88 +      if (text_field.isEditable && len > 0) {
    1.89 +        val caret = text_field.getCaret.getDot
    1.90 +        val content = text_field.getText
    1.91 +        JEdit_Lib.try_get_text(content, Text.Range(caret - len, caret)) match {
    1.92 +          case Some(text) if text == item.original =>
    1.93 +            text_field.setText(
    1.94 +              content.substring(0, caret - len) +
    1.95 +              item.replacement +
    1.96 +              content.substring(caret))
    1.97 +          case _ =>
    1.98 +        }
    1.99 +      }
   1.100 +    }
   1.101 +
   1.102 +
   1.103 +    /* completion action */
   1.104 +
   1.105 +    def action()
   1.106 +    {
   1.107 +      GUI.layered_pane(text_field) match {
   1.108 +        case Some(layered) if text_field.isEditable =>
   1.109 +          val history = PIDE.completion_history.value
   1.110 +
   1.111 +          val caret = text_field.getCaret.getDot
   1.112 +          val text = text_field.getText.substring(0, caret)
   1.113 +
   1.114 +          syntax.completion.complete(history, decode = true, explicit = false, text) match {
   1.115 +            case Some(result) =>
   1.116 +              val fm = text_field.getFontMetrics(text_field.getFont)
   1.117 +              val loc =
   1.118 +                SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
   1.119 +              val font =
   1.120 +                text_field.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   1.121 +
   1.122 +              val completion = new Completion_Popup(layered, loc, font, result.items)
   1.123 +              {
   1.124 +                override def complete(item: Completion.Item) {
   1.125 +                  PIDE.completion_history.update(item)
   1.126 +                  insert(item)
   1.127 +                }
   1.128 +                override def propagate(evt: KeyEvent) {
   1.129 +                  if (!evt.isConsumed) text_field.processKeyEvent(evt)
   1.130 +                }
   1.131 +                override def refocus() { text_field.requestFocus }
   1.132 +              }
   1.133 +              completion_popup = Some(completion)
   1.134 +              completion.show_popup()
   1.135 +
   1.136 +            case None =>
   1.137 +          }
   1.138 +        case _ =>
   1.139 +      }
   1.140 +    }
   1.141 +
   1.142 +
   1.143 +    /* process key event */
   1.144 +
   1.145 +    private def process(evt: KeyEvent)
   1.146 +    {
   1.147 +      if (PIDE.options.bool("jedit_completion")) {
   1.148 +        dismissed()
   1.149 +        if (evt.getKeyChar != '\b') {
   1.150 +          val special = JEdit_Lib.special_key(evt)
   1.151 +          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
   1.152 +            process_delay.revoke()
   1.153 +            action()
   1.154 +          }
   1.155 +          else process_delay.invoke()
   1.156 +        }
   1.157 +      }
   1.158 +    }
   1.159 +
   1.160 +    private val process_delay =
   1.161 +      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   1.162 +        action()
   1.163 +      }
   1.164 +
   1.165 +    override def processKeyEvent(evt0: KeyEvent)
   1.166 +    {
   1.167 +      val evt = KeyEventWorkaround.processKeyEvent(evt0)
   1.168 +      if (evt != null) {
   1.169 +        evt.getID match {
   1.170 +          case KeyEvent.KEY_PRESSED =>
   1.171 +            val key_code = evt.getKeyCode
   1.172 +            if (key_code == KeyEvent.VK_ESCAPE) {
   1.173 +              if (dismissed()) evt.consume
   1.174 +            }
   1.175 +          case KeyEvent.KEY_TYPED =>
   1.176 +            super.processKeyEvent(evt)
   1.177 +            process(evt)
   1.178 +            evt.consume
   1.179 +          case _ =>
   1.180 +        }
   1.181 +        if (!evt.isConsumed) super.processKeyEvent(evt)
   1.182 +      }
   1.183 +    }
   1.184 +  }
   1.185  }
   1.186  
   1.187  
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 14:30:34 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:07:34 2013 +0200
     2.3 @@ -18,7 +18,6 @@
     2.4  import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
     2.5  
     2.6  import org.gjt.sp.jedit.View
     2.7 -import org.gjt.sp.jedit.gui.HistoryTextField
     2.8  
     2.9  
    2.10  class Find_Dockable(view: View, position: String) extends Dockable(view, position)
    2.11 @@ -109,7 +108,7 @@
    2.12      tooltip = "Search criteria for find operation"
    2.13    }
    2.14  
    2.15 -  private val query = new HistoryTextField("isabelle-find-theorems") {
    2.16 +  private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
    2.17      override def processKeyEvent(evt: KeyEvent)
    2.18      {
    2.19        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
    2.20 @@ -118,6 +117,7 @@
    2.21      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
    2.22      setColumns(40)
    2.23      setToolTipText(query_label.tooltip)
    2.24 +    setFont(Token_Markup.imitate_font(Rendering.font_family(), getFont))
    2.25    }
    2.26  
    2.27    private case class Context_Entry(val name: String, val description: String)
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Sep 22 14:30:34 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Sep 22 18:07:34 2013 +0200
     3.3 @@ -10,12 +10,12 @@
     3.4  import isabelle._
     3.5  
     3.6  import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
     3.7 -import java.awt.event.{KeyEvent, KeyListener}
     3.8 +import java.awt.event.{InputEvent, KeyEvent, KeyListener}
     3.9  import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    3.10  
    3.11  import scala.annotation.tailrec
    3.12  
    3.13 -import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
    3.14 +import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
    3.15  import org.gjt.sp.jedit.gui.KeyEventWorkaround
    3.16  import org.gjt.sp.jedit.buffer.JEditBuffer
    3.17  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
    3.18 @@ -157,6 +157,10 @@
    3.19      try { Some(buffer.getText(range.start, range.length)) }
    3.20      catch { case _: ArrayIndexOutOfBoundsException => None }
    3.21  
    3.22 +  def try_get_text(text: String, range: Text.Range): Option[String] =
    3.23 +    try { Some(text.substring(range.start, range.stop)) }
    3.24 +    catch { case _: IndexOutOfBoundsException => None }
    3.25 +
    3.26  
    3.27    /* buffer range */
    3.28  
    3.29 @@ -336,5 +340,15 @@
    3.30        def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
    3.31      }
    3.32    }
    3.33 +
    3.34 +  def special_key(evt: KeyEvent): Boolean =
    3.35 +  {
    3.36 +    // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    3.37 +    val mod = evt.getModifiers
    3.38 +    (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    3.39 +    (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    3.40 +      !Debug.ALT_KEY_PRESSED_DISABLED ||
    3.41 +    (mod & InputEvent.META_MASK) != 0
    3.42 +  }
    3.43  }
    3.44  
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 14:30:34 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 18:07:34 2013 +0200
     4.3 @@ -73,13 +73,13 @@
     4.4    private def font_metrics(font: Font): LineMetrics =
     4.5      font.getLineMetrics("", new FontRenderContext(null, false, false))
     4.6  
     4.7 -  private def imitate_font(family: String, font: Font): Font =
     4.8 +  def imitate_font(family: String, font: Font): Font =
     4.9    {
    4.10 -    val font1 = new Font (family, font.getStyle, font.getSize)
    4.11 +    val font1 = new Font(family, font.getStyle, font.getSize)
    4.12      font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
    4.13    }
    4.14  
    4.15 -  private def transform_font(font: Font, transform: AffineTransform): Font =
    4.16 +  def transform_font(font: Font, transform: AffineTransform): Font =
    4.17    {
    4.18      import scala.collection.JavaConversions._
    4.19      font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))