src/Pure/General/completion.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/completion.ML	Sat Feb 22 20:52:43 2014 +0100
@@ -0,0 +1,37 @@
+(*  Title:      Pure/Isar/completion.ML
+    Author:     Makarius
+
+Completion within the formal context.
+*)
+
+signature COMPLETION =
+sig
+  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
+end;
+
+structure Completion: COMPLETION =
+struct
+
+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 =
+  Output.report (reported_text pos completion);
+
+end;