--- a/src/Pure/General/completion.ML Wed Mar 25 13:45:52 2015 +0100
+++ b/src/Pure/General/completion.ML Wed Mar 25 14:39:40 2015 +0100
@@ -9,6 +9,7 @@
type T
val names: Position.T -> (string * (string * string)) list -> T
val none: T
+ val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
val reported_text: T -> string
val suppress_abbrevs: string -> Markup.T list
end;
@@ -16,12 +17,12 @@
structure Completion: COMPLETION =
struct
+(* completion of names *)
+
abstype T =
Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
with
-(* completion of names *)
-
fun dest (Completion args) = args;
fun names pos names =
@@ -34,6 +35,11 @@
val none = names Position.none [];
+fun make (name, pos) make_names =
+ if Position.is_reported pos andalso name <> "" andalso name <> "_"
+ then names pos (make_names (String.isPrefix (Name.clean name)))
+ else none;
+
fun reported_text completion =
let val {pos, total, names} = dest completion in
if Position.is_reported pos andalso not (null names) then