some actual completion via outer syntax;
authorwenzelm
Tue Aug 27 20:45:02 2013 +0200 (2013-08-27)
changeset 532334b422e5d64fd
parent 53232 4a3762693452
child 53234 ea4abbbe1702
some actual completion via outer syntax;
disable old SideKick completion for "isabelle" mode;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 17:17:20 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 20:45:02 2013 +0200
     1.3 @@ -22,46 +22,83 @@
     1.4  
     1.5  object Completion_Popup
     1.6  {
     1.7 -  sealed case class Item(name: String, text: String)
     1.8 -  { override def toString: String = text }
     1.9 +  private sealed case class Item(original: String, replacement: String, description: String)
    1.10 +  { override def toString: String = description }
    1.11 +
    1.12 +  private def complete_item(text_area: JEditTextArea, item: Item)
    1.13 +  {
    1.14 +    Swing_Thread.require()
    1.15  
    1.16 -  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
    1.17 +    val buffer = text_area.getBuffer
    1.18 +    val len = item.original.length
    1.19 +    if (buffer.isEditable && len > 0) {
    1.20 +      JEdit_Lib.buffer_edit(buffer) {
    1.21 +        val caret = text_area.getCaretPosition
    1.22 +        JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    1.23 +          case Some(text) if text == item.original =>
    1.24 +            buffer.remove(caret - len, len)
    1.25 +            buffer.insert(caret - len, item.replacement)
    1.26 +          case _ =>
    1.27 +        }
    1.28 +      }
    1.29 +    }
    1.30 +  }
    1.31 +
    1.32 +  def input_text_area(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
    1.33    {
    1.34      Swing_Thread.require()
    1.35  
    1.36      val buffer = text_area.getBuffer
    1.37      if (buffer.isEditable) {
    1.38 -      val view = text_area.getView
    1.39 -      val painter = text_area.getPainter
    1.40 -      val caret = text_area.getCaretPosition
    1.41 +      get_syntax match {
    1.42 +        case None =>
    1.43 +        case Some(syntax) =>
    1.44 +          val view = text_area.getView
    1.45 +          val painter = text_area.getPainter
    1.46  
    1.47 -      // FIXME
    1.48 -      def complete(item: Item) { }
    1.49 -
    1.50 -      // FIXME
    1.51 -      val token_length = 0
    1.52 -      val items: List[Item] = Nil
    1.53 +          val caret = text_area.getCaretPosition
    1.54 +          val completion =
    1.55 +          {
    1.56 +            val line = buffer.getLineOfOffset(caret)
    1.57 +            val start = buffer.getLineStartOffset(line)
    1.58 +            val text = buffer.getSegment(start, caret - start)
    1.59  
    1.60 -      val popup_font =
    1.61 -        painter.getFont.deriveFont(
    1.62 -          (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    1.63 -            max 10.0f)
    1.64 +            syntax.completion.complete(text) match {
    1.65 +              case None => None
    1.66 +              case Some((word, cs)) =>
    1.67 +                val ds =
    1.68 +                  (if (Isabelle_Encoding.is_active(buffer))
    1.69 +                    cs.map(Symbol.decode(_)).sorted
    1.70 +                   else cs).filter(_ != word)
    1.71 +                if (ds.isEmpty) None
    1.72 +                else Some((word, ds.map(s => Item(word, s, s))))
    1.73 +            }
    1.74 +          }
    1.75 +          completion match {
    1.76 +            case None =>
    1.77 +            case Some((original, items)) =>
    1.78 +              val popup_font =
    1.79 +                painter.getFont.deriveFont(
    1.80 +                  (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    1.81 +                    max 10.0f)
    1.82  
    1.83 -      if (!items.isEmpty) {
    1.84 -        val location = text_area.offsetToXY(caret - token_length)
    1.85 -        if (location != null) {
    1.86 -          location.y = location.y + painter.getFontMetrics.getHeight
    1.87 -          SwingUtilities.convertPointToScreen(location, painter)
    1.88 -          new Completion_Popup(view.getRootPane, popup_font, location, items) {
    1.89 -            override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
    1.90 -            override def hidden() { text_area.requestFocus }
    1.91 +              val location = text_area.offsetToXY(caret - original.length)
    1.92 +              if (location != null) {
    1.93 +                location.y = location.y + painter.getFontMetrics.getHeight
    1.94 +                SwingUtilities.convertPointToScreen(location, painter)
    1.95 +                new Completion_Popup(view.getRootPane, popup_font, location, items) {
    1.96 +                  override def complete(item: Item) { complete_item(text_area, item) }
    1.97 +                  override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
    1.98 +                  override def hidden() { text_area.requestFocus }
    1.99 +                }
   1.100 +              }
   1.101            }
   1.102 -        }
   1.103        }
   1.104      }
   1.105    }
   1.106  }
   1.107  
   1.108 +
   1.109  class Completion_Popup private(
   1.110    root: JComponent,
   1.111    popup_font: Font,
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 17:17:20 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 20:45:02 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, _),
     2.8 +      key_typed = Completion_Popup.input_text_area(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())
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 27 17:17:20 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 27 20:45:02 2013 +0200
     3.3 @@ -188,6 +188,9 @@
     3.4  
     3.5  class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
     3.6    "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
     3.7 +{
     3.8 +  override def supportsCompletion = false
     3.9 +}
    3.10  
    3.11  
    3.12  class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(