clarified completion names;
authorwenzelm
Sun Feb 23 14:39:51 2014 +0100 (2014-02-23 ago)
changeset 5568778c83cd477c1
parent 55686 e99ed112d303
child 55688 767edb2c1e4e
clarified completion names;
tuned signature;
src/Pure/General/completion.ML
src/Pure/General/completion.scala
src/Pure/General/name_space.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/completion.ML	Sun Feb 23 10:44:57 2014 +0100
     1.2 +++ b/src/Pure/General/completion.ML	Sun Feb 23 14:39:51 2014 +0100
     1.3 @@ -6,32 +6,40 @@
     1.4  
     1.5  signature COMPLETION =
     1.6  sig
     1.7 -  val limit: unit -> int
     1.8 -  type T = {original: string, replacements: string list}
     1.9 +  type T
    1.10 +  val make: Position.T -> string list -> T
    1.11    val none: T
    1.12 -  val reported_text: Position.T -> T -> string
    1.13 -  val report: Position.T -> T -> unit
    1.14 +  val report: T -> unit
    1.15  end;
    1.16  
    1.17  structure Completion: COMPLETION =
    1.18  struct
    1.19  
    1.20 -fun limit () = Options.default_int "completion_limit";
    1.21 -
    1.22 +abstype T = Completion of {pos: Position.T, total: int, names: string list}
    1.23 +with
    1.24  
    1.25 -type T = {original: string, replacements: string list};
    1.26 -
    1.27 -val none: T = {original = "", replacements = []};
    1.28 +fun dest (Completion args) = args;
    1.29  
    1.30 -fun encode ({original, replacements}: T) =
    1.31 -  (original, replacements)
    1.32 -  |> let open XML.Encode in pair string (list string) end;
    1.33 -
    1.34 -fun reported_text pos (completion: T) =
    1.35 -  if null (#replacements completion) then ""
    1.36 -  else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
    1.37 -
    1.38 -fun report pos completion =
    1.39 -  Output.report (reported_text pos completion);
    1.40 +fun make pos names =
    1.41 +  Completion
    1.42 +   {pos = pos,
    1.43 +    total = length names,
    1.44 +    names = take (Options.default_int "completion_limit") names};
    1.45  
    1.46  end;
    1.47 +
    1.48 +val none = make Position.none [];
    1.49 +
    1.50 +fun report completion =
    1.51 +  let val {pos, total, names} = dest completion in
    1.52 +    if Position.is_reported pos andalso not (null names) then
    1.53 +      let
    1.54 +        val props =
    1.55 +          (Markup.totalN, Markup.print_int total) ::
    1.56 +            (map Markup.print_int (1 upto length names) ~~ names);
    1.57 +        val markup = (Markup.completionN, Position.properties_of pos @ props);
    1.58 +      in Output.report (Markup.markup markup "") end
    1.59 +    else ()
    1.60 +  end;
    1.61 +
    1.62 +end;
     2.1 --- a/src/Pure/General/completion.scala	Sun Feb 23 10:44:57 2014 +0100
     2.2 +++ b/src/Pure/General/completion.scala	Sun Feb 23 14:39:51 2014 +0100
     2.3 @@ -1,10 +1,9 @@
     2.4  /*  Title:      Pure/General/completion.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Semantic completion within the formal context (reported by prover).
     2.8 +Semantic completion within the formal context (reported names).
     2.9  Syntactic completion of keywords and symbols, with abbreviations
    2.10 -(based on language context).
    2.11 -*/
    2.12 +(based on language context).  */
    2.13  
    2.14  package isabelle
    2.15  
    2.16 @@ -18,30 +17,21 @@
    2.17  {
    2.18    /** semantic completion **/
    2.19  
    2.20 -  object Reported
    2.21 +  object Names
    2.22    {
    2.23 -    object Elem
    2.24 +    object Info
    2.25      {
    2.26 -      private def decode: XML.Decode.T[(String, List[String])] =
    2.27 -      {
    2.28 -        import XML.Decode._
    2.29 -        pair(string, list(string))
    2.30 -      }
    2.31 -
    2.32 -      def unapply(tree: XML.Tree): Option[Reported] =
    2.33 -        tree match {
    2.34 -          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
    2.35 -            try {
    2.36 -              val (original, replacements) = decode(body)
    2.37 -              Some(Reported(original, replacements))
    2.38 -            }
    2.39 -            catch { case _: XML.Error => None }
    2.40 +      def unapply(info: Text.Markup): Option[Names] =
    2.41 +        info.info match {
    2.42 +          case XML.Elem(Markup(Markup.COMPLETION,
    2.43 +              (Markup.TOTAL, Properties.Value.Int(total)) :: names), _) =>
    2.44 +            Some(Names(info.range, total, names.map(_._2)))
    2.45            case _ => None
    2.46          }
    2.47      }
    2.48    }
    2.49  
    2.50 -  sealed case class Reported(original: String, replacements: List[String])
    2.51 +  sealed case class Names(range: Text.Range, total: Int, names: List[String])
    2.52  
    2.53  
    2.54  
     3.1 --- a/src/Pure/General/name_space.ML	Sun Feb 23 10:44:57 2014 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Sun Feb 23 14:39:51 2014 +0100
     3.3 @@ -205,13 +205,12 @@
     3.4  fun completion context (space as Name_Space {internals, ...}) (xname, pos) =
     3.5    if Context_Position.is_visible_generic context andalso Position.is_reported pos then
     3.6      let
     3.7 -      val replacements =
     3.8 +      val names =
     3.9          Symtab.fold (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons b | _ => I)
    3.10            internals []
    3.11 -        |> take (Completion.limit ())
    3.12          |> map (extern_shortest (Context.proof_of context) space)
    3.13          |> sort_distinct string_ord;
    3.14 -    in {original = xname, replacements = replacements} end
    3.15 +    in Completion.make pos names end
    3.16    else Completion.none;
    3.17  
    3.18  
    3.19 @@ -447,7 +446,7 @@
    3.20      (case Symtab.lookup tab name of
    3.21        SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
    3.22      | NONE =>
    3.23 -       (Completion.report pos (completion context space (xname, pos));
    3.24 +       (Completion.report (completion context space (xname, pos));
    3.25          error (undefined (kind_of space) name ^ Position.here pos)))
    3.26    end;
    3.27  
     4.1 --- a/src/Pure/PIDE/markup.ML	Sun Feb 23 10:44:57 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sun Feb 23 14:39:51 2014 +0100
     4.3 @@ -37,7 +37,8 @@
     4.4    val get_entity_kind: T -> string option
     4.5    val defN: string
     4.6    val refN: string
     4.7 -  val completionN: string val completion: T
     4.8 +  val totalN: string
     4.9 +  val completionN: string
    4.10    val lineN: string
    4.11    val offsetN: string
    4.12    val end_offsetN: string
    4.13 @@ -286,7 +287,8 @@
    4.14  
    4.15  (* completion *)
    4.16  
    4.17 -val (completionN, completion) = markup_elem "completion";
    4.18 +val totalN = "total";
    4.19 +val completionN = "completion";
    4.20  
    4.21  
    4.22  (* position *)
     5.1 --- a/src/Pure/PIDE/markup.scala	Sun Feb 23 10:44:57 2014 +0100
     5.2 +++ b/src/Pure/PIDE/markup.scala	Sun Feb 23 14:39:51 2014 +0100
     5.3 @@ -69,6 +69,7 @@
     5.4  
     5.5    /* completion */
     5.6  
     5.7 +  val TOTAL = "total"
     5.8    val COMPLETION = "completion"
     5.9  
    5.10  
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 10:44:57 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 14:39:51 2014 +0100
     6.3 @@ -150,7 +150,7 @@
     6.4  
     6.5    /* markup elements */
     6.6  
     6.7 -  private val completion_reported_elements = Set(Markup.COMPLETION)
     6.8 +  private val completion_names_elements = Set(Markup.COMPLETION)
     6.9  
    6.10    private val completion_context_elements =
    6.11      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    6.12 @@ -273,20 +273,17 @@
    6.13  
    6.14    /* completion */
    6.15  
    6.16 -  def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
    6.17 -    if (caret > 0)
    6.18 +  def completion_names(caret: Text.Offset): Option[Completion.Names] =
    6.19 +    if (caret > 0 && !snapshot.is_outdated)
    6.20      {
    6.21        val result =
    6.22          snapshot.select(Text.Range(caret - 1, caret + 1),
    6.23 -          Rendering.completion_reported_elements, _ =>
    6.24 +          Rendering.completion_names_elements, _ =>
    6.25            {
    6.26 -            case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
    6.27 +            case Completion.Names.Info(names) => Some(names)
    6.28              case _ => None
    6.29            })
    6.30 -      result match {
    6.31 -        case Text.Info(_, reported) :: _ => Some(reported)
    6.32 -        case Nil => None
    6.33 -      }
    6.34 +      result.headOption.map(_.info)
    6.35      }
    6.36      else None
    6.37  
    6.38 @@ -304,10 +301,7 @@
    6.39              case Text.Info(_, _) =>
    6.40                Some(Completion.Context.inner)
    6.41            })
    6.42 -      result match {
    6.43 -        case Text.Info(_, context) :: _ => Some(context)
    6.44 -        case Nil => None
    6.45 -      }
    6.46 +      result.headOption.map(_.info)
    6.47      }
    6.48      else None
    6.49