src/Tools/jEdit/src/completion_popup.scala
changeset 53275 b34aac6511ab
parent 53274 1760c01f1c78
child 53292 f567c1c7b180
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 12:38:33 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 13:00:59 2013 +0200
     1.3 @@ -22,12 +22,6 @@
     1.4  
     1.5  object Completion_Popup
     1.6  {
     1.7 -  /* items */
     1.8 -
     1.9 -  private sealed case class Item(original: String, replacement: String, description: String)
    1.10 -  { override def toString: String = description }
    1.11 -
    1.12 -
    1.13    /* setup for jEdit text area */
    1.14  
    1.15    object Text_Area
    1.16 @@ -93,7 +87,7 @@
    1.17  
    1.18      /* insert selected item */
    1.19  
    1.20 -    private def insert(item: Item)
    1.21 +    private def insert(item: Completion.Item)
    1.22      {
    1.23        Swing_Thread.require()
    1.24  
    1.25 @@ -143,24 +137,11 @@
    1.26            Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.27              case Some(syntax) =>
    1.28                val caret = text_area.getCaretPosition
    1.29 -              val result =
    1.30 -              {
    1.31 -                val line = buffer.getLineOfOffset(caret)
    1.32 -                val start = buffer.getLineStartOffset(line)
    1.33 -                val text = buffer.getSegment(start, caret - start)
    1.34 +              val line = buffer.getLineOfOffset(caret)
    1.35 +              val start = buffer.getLineStartOffset(line)
    1.36 +              val text = buffer.getSegment(start, caret - start)
    1.37  
    1.38 -                syntax.completion.complete(text) match {
    1.39 -                  case Some((word, cs)) =>
    1.40 -                    val ds =
    1.41 -                      (if (Isabelle_Encoding.is_active(buffer))
    1.42 -                        cs.map(Symbol.decode(_)).sorted
    1.43 -                       else cs).filter(_ != word)
    1.44 -                    if (ds.isEmpty) None
    1.45 -                    else Some((word, ds.map(s => Item(word, s, s))))
    1.46 -                  case None => None
    1.47 -                }
    1.48 -              }
    1.49 -              result match {
    1.50 +              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    1.51                  case Some((original, items)) =>
    1.52                    val font =
    1.53                      painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.54 @@ -173,10 +154,10 @@
    1.55  
    1.56                      val completion =
    1.57                        new Completion_Popup(layered, loc2, font, items) {
    1.58 -                        override def complete(item: Item) { insert(item) }
    1.59 -                        override def propagate(e: KeyEvent) {
    1.60 -                          JEdit_Lib.propagate_key(view, e)
    1.61 -                          input(e)
    1.62 +                        override def complete(item: Completion.Item) { insert(item) }
    1.63 +                        override def propagate(evt: KeyEvent) {
    1.64 +                          JEdit_Lib.propagate_key(view, evt)
    1.65 +                          input(evt)
    1.66                          }
    1.67                          override def refocus() { text_area.requestFocus }
    1.68                        }
    1.69 @@ -214,7 +195,7 @@
    1.70    layered: JLayeredPane,
    1.71    location: Point,
    1.72    font: Font,
    1.73 -  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
    1.74 +  items: List[Completion.Item]) extends JPanel(new BorderLayout)
    1.75  {
    1.76    completion =>
    1.77  
    1.78 @@ -224,7 +205,7 @@
    1.79  
    1.80    /* actions */
    1.81  
    1.82 -  def complete(item: Completion_Popup.Item) { }
    1.83 +  def complete(item: Completion.Item) { }
    1.84    def propagate(evt: KeyEvent) { }
    1.85    def refocus() { }
    1.86