more detailed description of completion items;
authorwenzelm
Fri Mar 07 14:37:25 2014 +0100 (2014-03-07)
changeset 55977ec4830499634
parent 55976 43815ee659bc
child 55978 56645c447ee9
more detailed description of completion items;
src/Pure/General/completion.ML
src/Pure/General/completion.scala
src/Pure/General/name_space.ML
src/Pure/library.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/completion.ML	Fri Mar 07 13:29:10 2014 +0100
     1.2 +++ b/src/Pure/General/completion.ML	Fri Mar 07 14:37:25 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature COMPLETION =
     1.5  sig
     1.6    type T
     1.7 -  val names: Position.T -> (string * string) list -> T
     1.8 +  val names: Position.T -> (string * (string * string)) list -> T
     1.9    val none: T
    1.10    val reported_text: T -> string
    1.11    val report: T -> unit
    1.12 @@ -17,7 +17,8 @@
    1.13  structure Completion: COMPLETION =
    1.14  struct
    1.15  
    1.16 -abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
    1.17 +abstype T =
    1.18 +  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
    1.19  with
    1.20  
    1.21  (* completion of names *)
    1.22 @@ -40,7 +41,7 @@
    1.23        let
    1.24          val markup = Position.markup pos Markup.completion;
    1.25          val body = (total, names) |>
    1.26 -          let open XML.Encode in pair int (list (pair string string)) end;
    1.27 +          let open XML.Encode in pair int (list (pair string (pair string string))) end;
    1.28        in YXML.string_of (XML.Elem (markup, body)) end
    1.29      else ""
    1.30    end;
     2.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 13:29:10 2014 +0100
     2.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 14:37:25 2014 +0100
     2.3 @@ -136,7 +136,7 @@
     2.4                val (total, names) =
     2.5                {
     2.6                  import XML.Decode._
     2.7 -                pair(int, list(pair(string, string)))(body)
     2.8 +                pair(int, list(pair(string, pair(string, string))))(body)
     2.9                }
    2.10                Some(Names(info.range, total, names))
    2.11              }
    2.12 @@ -148,21 +148,27 @@
    2.13      }
    2.14    }
    2.15  
    2.16 -  sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
    2.17 +  sealed case class Names(
    2.18 +    range: Text.Range, total: Int, names: List[(String, (String, String))])
    2.19    {
    2.20      def no_completion: Boolean = total == 0 && names.isEmpty
    2.21  
    2.22      def complete(
    2.23        history: Completion.History,
    2.24 -      decode: Boolean,
    2.25 +      do_decode: Boolean,
    2.26        original: String): Option[Completion.Result] =
    2.27      {
    2.28 +      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
    2.29        val items =
    2.30          for {
    2.31 -          (xname, name) <- names
    2.32 -          xname1 = (if (decode) Symbol.decode(xname) else xname)
    2.33 +          (xname, (kind, name)) <- names
    2.34 +          xname1 = decode(xname)
    2.35            if xname1 != original
    2.36 -        } yield Item(range, original, name, xname1, xname1, 0, true)
    2.37 +          (full_name, descr_name) =
    2.38 +            if (kind == "") (name, quote(decode(name)))
    2.39 +            else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
    2.40 +          description = xname1 + "   (" + descr_name + ")"
    2.41 +        } yield Item(range, original, full_name, description, xname1, 0, true)
    2.42  
    2.43        if (items.isEmpty) None
    2.44        else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
    2.45 @@ -298,7 +304,7 @@
    2.46  
    2.47    def complete(
    2.48      history: Completion.History,
    2.49 -    decode: Boolean,
    2.50 +    do_decode: Boolean,
    2.51      explicit: Boolean,
    2.52      start: Text.Offset,
    2.53      text: CharSequence,
    2.54 @@ -306,6 +312,7 @@
    2.55      extend_word: Boolean,
    2.56      language_context: Completion.Language_Context): Option[Completion.Result] =
    2.57    {
    2.58 +    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
    2.59      val length = text.length
    2.60  
    2.61      val abbrevs_result =
    2.62 @@ -356,21 +363,28 @@
    2.63      words_result match {
    2.64        case Some(((word, cs), end)) =>
    2.65          val range = Text.Range(- word.length, 0) + end + start
    2.66 -        val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
    2.67 +        val ds = cs.map(decode(_)).filter(_ != word)
    2.68          if (ds.isEmpty) None
    2.69          else {
    2.70            val immediate =
    2.71              !Completion.Word_Parsers.is_word(word) &&
    2.72              Character.codePointCount(word, 0, word.length) > 1
    2.73            val items =
    2.74 -            ds.map(s => {
    2.75 +            for { (name, name1) <- cs zip ds }
    2.76 +            yield {
    2.77                val (s1, s2) =
    2.78 -                space_explode(Completion.caret_indicator, s) match {
    2.79 +                space_explode(Completion.caret_indicator, name1) match {
    2.80                    case List(s1, s2) => (s1, s2)
    2.81 -                  case _ => (s, "")
    2.82 +                  case _ => (name1, "")
    2.83                  }
    2.84 -              Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
    2.85 -            })
    2.86 +              val description =
    2.87 +                if (keywords(name)) name1 + "   (keyword)"
    2.88 +                else if (Symbol.names.isDefinedAt(name) && name != name1)
    2.89 +                  name1 + "   (symbol " + quote(name) + ")"
    2.90 +                else name1
    2.91 +              Completion.Item(
    2.92 +                range, word, name1, description, s1 + s2, - s2.length, explicit || immediate)
    2.93 +            }
    2.94            Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
    2.95          }
    2.96        case None => None
     3.1 --- a/src/Pure/General/name_space.ML	Fri Mar 07 13:29:10 2014 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 07 14:37:25 2014 +0100
     3.3 @@ -214,7 +214,7 @@
     3.4          Symtab.fold
     3.5            (fn (a, (name :: _, _)) =>
     3.6                if String.isPrefix x a andalso not (is_concealed space name)
     3.7 -              then cons (ext name, Long_Name.implode [kind, name]) else I
     3.8 +              then cons (ext name, (kind, name)) else I
     3.9              | _ => I) internals []
    3.10          |> sort_distinct (string_ord o pairself #1);
    3.11      in Completion.names pos names end
     4.1 --- a/src/Pure/library.scala	Fri Mar 07 13:29:10 2014 +0100
     4.2 +++ b/src/Pure/library.scala	Fri Mar 07 14:37:25 2014 +0100
     4.3 @@ -97,6 +97,9 @@
     4.4      else ""
     4.5    }
     4.6  
     4.7 +  def plain_words(str: String): String =
     4.8 +    space_explode('_', str).mkString(" ")
     4.9 +
    4.10  
    4.11    /* strings */
    4.12  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 13:29:10 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 14:37:25 2014 +0100
     5.3 @@ -459,7 +459,7 @@
     5.4            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
     5.5              Some(Text.Info(r, (t1 + t2, info)))
     5.6            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
     5.7 -            val kind1 = space_explode('_', kind).mkString(" ")
     5.8 +            val kind1 = Library.plain_words(kind)
     5.9              val txt1 = kind1 + " " + quote(name)
    5.10              val t = prev.info._1
    5.11              val txt2 =