tuned signature;
authorwenzelm
Wed Aug 28 09:08:36 2013 +0200 (2013-08-28)
changeset 53242142f4fff4e40
parent 53241 effd8fcabca2
child 53243 dabe46c68228
tuned signature;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 00:18:50 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 09:08:36 2013 +0200
     1.3 @@ -44,83 +44,86 @@
     1.4  
     1.5    /* jEdit text area operations */
     1.6  
     1.7 -  private def complete_text_area(text_area: JEditTextArea, item: Item)
     1.8 +  object Text_Area
     1.9    {
    1.10 -    Swing_Thread.require()
    1.11 +    private def insert(text_area: JEditTextArea, item: Item)
    1.12 +    {
    1.13 +      Swing_Thread.require()
    1.14  
    1.15 -    val buffer = text_area.getBuffer
    1.16 -    val len = item.original.length
    1.17 -    if (buffer.isEditable && len > 0) {
    1.18 -      JEdit_Lib.buffer_edit(buffer) {
    1.19 -        val caret = text_area.getCaretPosition
    1.20 -        JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    1.21 -          case Some(text) if text == item.original =>
    1.22 -            buffer.remove(caret - len, len)
    1.23 -            buffer.insert(caret - len, item.replacement)
    1.24 -          case _ =>
    1.25 +      val buffer = text_area.getBuffer
    1.26 +      val len = item.original.length
    1.27 +      if (buffer.isEditable && len > 0) {
    1.28 +        JEdit_Lib.buffer_edit(buffer) {
    1.29 +          val caret = text_area.getCaretPosition
    1.30 +          JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    1.31 +            case Some(text) if text == item.original =>
    1.32 +              buffer.remove(caret - len, len)
    1.33 +              buffer.insert(caret - len, item.replacement)
    1.34 +            case _ =>
    1.35 +          }
    1.36          }
    1.37        }
    1.38      }
    1.39 -  }
    1.40 +
    1.41 +    def input(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
    1.42 +    {
    1.43 +      Swing_Thread.require()
    1.44  
    1.45 -  def input_text_area(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
    1.46 -  {
    1.47 -    Swing_Thread.require()
    1.48 -
    1.49 -    val view = text_area.getView
    1.50 -    val root = view.getRootPane
    1.51 -    val buffer = text_area.getBuffer
    1.52 -    val painter = text_area.getPainter
    1.53 +      val view = text_area.getView
    1.54 +      val root = view.getRootPane
    1.55 +      val buffer = text_area.getBuffer
    1.56 +      val painter = text_area.getPainter
    1.57  
    1.58 -    register(root, null)
    1.59 +      register(root, null)
    1.60  
    1.61 -    if (buffer.isEditable) {
    1.62 -      get_syntax match {
    1.63 -        case Some(syntax) =>
    1.64 -          val caret = text_area.getCaretPosition
    1.65 -          val result =
    1.66 -          {
    1.67 -            val line = buffer.getLineOfOffset(caret)
    1.68 -            val start = buffer.getLineStartOffset(line)
    1.69 -            val text = buffer.getSegment(start, caret - start)
    1.70 +      if (buffer.isEditable) {
    1.71 +        get_syntax match {
    1.72 +          case Some(syntax) =>
    1.73 +            val caret = text_area.getCaretPosition
    1.74 +            val result =
    1.75 +            {
    1.76 +              val line = buffer.getLineOfOffset(caret)
    1.77 +              val start = buffer.getLineStartOffset(line)
    1.78 +              val text = buffer.getSegment(start, caret - start)
    1.79  
    1.80 -            syntax.completion.complete(text) match {
    1.81 -              case Some((word, cs)) =>
    1.82 -                val ds =
    1.83 -                  (if (Isabelle_Encoding.is_active(buffer))
    1.84 -                    cs.map(Symbol.decode(_)).sorted
    1.85 -                   else cs).filter(_ != word)
    1.86 -                if (ds.isEmpty) None
    1.87 -                else Some((word, ds.map(s => Item(word, s, s))))
    1.88 -              case None => None
    1.89 +              syntax.completion.complete(text) match {
    1.90 +                case Some((word, cs)) =>
    1.91 +                  val ds =
    1.92 +                    (if (Isabelle_Encoding.is_active(buffer))
    1.93 +                      cs.map(Symbol.decode(_)).sorted
    1.94 +                     else cs).filter(_ != word)
    1.95 +                  if (ds.isEmpty) None
    1.96 +                  else Some((word, ds.map(s => Item(word, s, s))))
    1.97 +                case None => None
    1.98 +              }
    1.99              }
   1.100 -          }
   1.101 -          result match {
   1.102 -            case Some((original, items)) =>
   1.103 -              val popup_font =
   1.104 -                painter.getFont.deriveFont(
   1.105 -                  (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
   1.106 -                    max 10.0f)
   1.107 +            result match {
   1.108 +              case Some((original, items)) =>
   1.109 +                val popup_font =
   1.110 +                  painter.getFont.deriveFont(
   1.111 +                    (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
   1.112 +                      max 10.0f)
   1.113  
   1.114 -              val location = text_area.offsetToXY(caret - original.length)
   1.115 -              if (location != null) {
   1.116 -                location.y = location.y + painter.getFontMetrics.getHeight
   1.117 -                SwingUtilities.convertPointToScreen(location, painter)
   1.118 +                val location = text_area.offsetToXY(caret - original.length)
   1.119 +                if (location != null) {
   1.120 +                  location.y = location.y + painter.getFontMetrics.getHeight
   1.121 +                  SwingUtilities.convertPointToScreen(location, painter)
   1.122  
   1.123 -                val completion =
   1.124 -                  new Completion_Popup(root, popup_font, location, items) {
   1.125 -                    override def complete(item: Item) { complete_text_area(text_area, item) }
   1.126 -                    override def propagate(e: KeyEvent) {
   1.127 -                      JEdit_Lib.propagate_key(view, e)
   1.128 -                      if (!e.isConsumed) input_text_area(text_area, get_syntax, e)
   1.129 +                  val completion =
   1.130 +                    new Completion_Popup(root, popup_font, location, items) {
   1.131 +                      override def complete(item: Item) { insert(text_area, item) }
   1.132 +                      override def propagate(e: KeyEvent) {
   1.133 +                        JEdit_Lib.propagate_key(view, e)
   1.134 +                        if (!e.isConsumed) input(text_area, get_syntax, e)
   1.135 +                      }
   1.136 +                      override def refocus() { text_area.requestFocus }
   1.137                      }
   1.138 -                    override def refocus() { text_area.requestFocus }
   1.139 -                  }
   1.140 -                register(root, completion)
   1.141 -              }
   1.142 -            case None =>
   1.143 -          }
   1.144 -        case None =>
   1.145 +                  register(root, completion)
   1.146 +                }
   1.147 +              case None =>
   1.148 +            }
   1.149 +          case None =>
   1.150 +        }
   1.151        }
   1.152      }
   1.153    }
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 00:18:50 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:08:36 2013 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4  
     2.5    private val key_listener =
     2.6      JEdit_Lib.key_listener(
     2.7 -      key_typed = Completion_Popup.input_text_area(text_area, PIDE.get_recent_syntax, _),
     2.8 +      key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
     2.9        key_pressed = (evt: KeyEvent) =>
    2.10          {
    2.11            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())