clarified boundary cases of completion;
authorwenzelm
Thu Jul 16 16:30:43 2015 +0200 (2015-07-16)
changeset 6073218299765542e
parent 60731 4ac4b314d93c
child 60733 7a72429c5a1f
clarified boundary cases of completion;
src/Pure/General/completion.scala
src/Pure/ML/ml_compiler_polyml.ML
     1.1 --- a/src/Pure/General/completion.scala	Thu Jul 16 14:40:23 2015 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Thu Jul 16 16:30:43 2015 +0200
     1.3 @@ -199,7 +199,8 @@
     1.4              if (kind == "") (name, quote(decode(name)))
     1.5              else
     1.6               (Long_Name.qualify(kind, name),
     1.7 -              Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
     1.8 +              Word.implode(Word.explode('_', kind)) +
     1.9 +              (if (xname == name) "" else " " + quote(decode(name))))
    1.10            description = List(xname1, "(" + descr_name + ")")
    1.11          } yield Item(range, original, full_name, description, xname1, 0, true)
    1.12  
     2.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 14:40:23 2015 +0200
     2.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 16:30:43 2015 +0200
     2.3 @@ -45,9 +45,9 @@
     2.4  
     2.5      fun reported_completions loc names =
     2.6        let val pos = Exn_Properties.position_of loc in
     2.7 -        if is_reported pos then
     2.8 +        if is_reported pos andalso not (null names) then
     2.9            let
    2.10 -            val completion = Completion.names pos (map (fn a => (a, ("ML", ""))) names);
    2.11 +            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    2.12              val xml = Completion.encode completion;
    2.13            in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
    2.14          else I