--- a/src/Pure/General/completion.ML Wed Mar 05 13:11:08 2014 +0100
+++ b/src/Pure/General/completion.ML Wed Mar 05 14:19:54 2014 +0100
@@ -11,6 +11,7 @@
val none: T
val reported_text: T -> string
val report: T -> unit
+ val suppress_abbrevs: string -> Markup.T list
end;
structure Completion: COMPLETION =
@@ -19,6 +20,8 @@
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 =
@@ -44,4 +47,12 @@
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;