author wenzelm
Sat, 22 Feb 2014 20:52:43 +0100
changeset 55672 5e25cc741ab9
child 55674 8a213ab0e78a
permissions -rw-r--r--
support for completion within the formal context; tuned signature;

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

Completion within the formal context.

signature COMPLETION =
  val limit: unit -> int
  type T = {original: string, replacements: string list}
  val none: T
  val reported_text: Position.T -> T -> string
  val report: Position.T -> T -> unit

structure Completion: COMPLETION =

fun limit () = Options.default_int "completion_limit";

type T = {original: string, replacements: string list};

val none: T = {original = "", replacements = []};

fun encode ({original, replacements}: T) =
  (original, replacements)
  |> let open XML.Encode in pair string (list string) end;

fun reported_text pos (completion: T) =
  if null (#replacements completion) then ""
  else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));

fun report pos completion = (reported_text pos completion);