tuned description and its rendering;
authorwenzelm
Fri Mar 07 15:16:08 2014 +0100 (2014-03-07)
changeset 5597856645c447ee9
parent 55977 ec4830499634
child 55979 06cb126f30ba
tuned description and its rendering;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 14:37:25 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 15:16:08 2014 +0100
     1.3 @@ -21,11 +21,10 @@
     1.4      range: Text.Range,
     1.5      original: String,
     1.6      name: String,
     1.7 -    description: String,
     1.8 +    description: List[String],
     1.9      replacement: String,
    1.10      move: Int,
    1.11      immediate: Boolean)
    1.12 -  { override def toString: String = description }
    1.13  
    1.14    object Result
    1.15    {
    1.16 @@ -167,7 +166,7 @@
    1.17            (full_name, descr_name) =
    1.18              if (kind == "") (name, quote(decode(name)))
    1.19              else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
    1.20 -          description = xname1 + "   (" + descr_name + ")"
    1.21 +          description = List(xname1, "(" + descr_name + ")")
    1.22          } yield Item(range, original, full_name, description, xname1, 0, true)
    1.23  
    1.24        if (items.isEmpty) None
    1.25 @@ -377,13 +376,14 @@
    1.26                    case List(s1, s2) => (s1, s2)
    1.27                    case _ => (name1, "")
    1.28                  }
    1.29 +              val move = - s2.length
    1.30                val description =
    1.31 -                if (keywords(name)) name1 + "   (keyword)"
    1.32 +                if (move != 0) List(name1, "(template)")
    1.33 +                else if (keywords(name)) List(name1, "(keyword)")
    1.34                  else if (Symbol.names.isDefinedAt(name) && name != name1)
    1.35 -                  name1 + "   (symbol " + quote(name) + ")"
    1.36 -                else name1
    1.37 -              Completion.Item(
    1.38 -                range, word, name1, description, s1 + s2, - s2.length, explicit || immediate)
    1.39 +                  List(name1, "(symbol " + quote(name) + ")")
    1.40 +                else List(name1)
    1.41 +              Completion.Item(range, word, name1, description, s1 + s2, move, explicit || immediate)
    1.42              }
    1.43            Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
    1.44          }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 14:37:25 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 07 15:16:08 2014 +0100
     2.3 @@ -25,6 +25,22 @@
     2.4  
     2.5  object Completion_Popup
     2.6  {
     2.7 +  /** items with HTML rendering **/
     2.8 +
     2.9 +  private class Item(val item: Completion.Item)
    2.10 +  {
    2.11 +    private val html =
    2.12 +      item.description match {
    2.13 +        case a :: bs =>
    2.14 +          "<html><b>" + HTML.encode(a) + "</b>" +
    2.15 +            HTML.encode(bs.map(" " + _).mkString) + "</html>"
    2.16 +        case Nil => ""
    2.17 +      }
    2.18 +    override def toString: String = html
    2.19 +  }
    2.20 +
    2.21 +
    2.22 +
    2.23    /** jEdit text area **/
    2.24  
    2.25    object Text_Area
    2.26 @@ -210,8 +226,10 @@
    2.27              SwingUtilities.convertPoint(painter,
    2.28                loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    2.29  
    2.30 +          val items = result.items.map(new Item(_))
    2.31            val completion =
    2.32 -            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
    2.33 +            new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
    2.34 +            {
    2.35                override def complete(item: Completion.Item) {
    2.36                  PIDE.completion_history.update(item)
    2.37                  insert(item)
    2.38 @@ -402,18 +420,19 @@
    2.39                val loc =
    2.40                  SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
    2.41  
    2.42 +              val items = result.items.map(new Item(_))
    2.43                val completion =
    2.44 -                new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
    2.45 -              {
    2.46 -                override def complete(item: Completion.Item) {
    2.47 -                  PIDE.completion_history.update(item)
    2.48 -                  insert(item)
    2.49 +                new Completion_Popup(None, layered, loc, text_field.getFont, items)
    2.50 +                {
    2.51 +                  override def complete(item: Completion.Item) {
    2.52 +                    PIDE.completion_history.update(item)
    2.53 +                    insert(item)
    2.54 +                  }
    2.55 +                  override def propagate(evt: KeyEvent) {
    2.56 +                    if (!evt.isConsumed) text_field.processKeyEvent(evt)
    2.57 +                  }
    2.58 +                  override def refocus() { text_field.requestFocus }
    2.59                  }
    2.60 -                override def propagate(evt: KeyEvent) {
    2.61 -                  if (!evt.isConsumed) text_field.processKeyEvent(evt)
    2.62 -                }
    2.63 -                override def refocus() { text_field.requestFocus }
    2.64 -              }
    2.65                completion_popup = Some(completion)
    2.66                completion.show_popup()
    2.67  
    2.68 @@ -474,7 +493,7 @@
    2.69    layered: JLayeredPane,
    2.70    location: Point,
    2.71    font: Font,
    2.72 -  items: List[Completion.Item]) extends JPanel(new BorderLayout)
    2.73 +  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
    2.74  {
    2.75    completion =>
    2.76  
    2.77 @@ -508,7 +527,7 @@
    2.78    private def complete_selected(): Boolean =
    2.79    {
    2.80      list_view.selection.items.toList match {
    2.81 -      case item :: _ => complete(item); true
    2.82 +      case item :: _ => complete(item.item); true
    2.83        case _ => false
    2.84      }
    2.85    }