src/Pure/General/completion.ML

suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
tuned signature;

(*  Title:      Pure/Isar/completion.ML
    Author:     Makarius

Semantic completion within the formal context.
*)

signature COMPLETION =
sig
  type T
  val names: Position.T -> (string * string) list -> T
  val none: T
  val reported_text: T -> string
  val report: T -> unit
  val suppress_abbrevs: string -> Markup.T list
end;

structure Completion: COMPLETION =
struct

abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
with

(* completion of names *)

fun dest (Completion args) = args;

fun names pos names =
  Completion
   {pos = pos,
    total = length names,
    names = take (Options.default_int "completion_limit") names};

end;

val none = names Position.none [];

fun reported_text completion =
  let val {pos, total, names} = dest completion in
    if Position.is_reported pos andalso not (null names) then
      let
        val markup = Position.markup pos Markup.completion;
        val body = (total, names) |>
          let open XML.Encode in pair int (list (pair string string)) end;
      in YXML.string_of (XML.Elem (markup, body)) end
    else ""
  end;

val report = Output.report o reported_text;


(* suppress short abbreviations *)

fun suppress_abbrevs s =
  if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) = 1 orelse s = "::")
  then [Markup.no_completion]
  else [];

end;