--- a/src/Pure/General/name_space.ML Thu Oct 25 14:04:37 2018 +0200
+++ b/src/Pure/General/name_space.ML Thu Oct 25 15:41:40 2018 +0200
@@ -30,7 +30,7 @@
val extern_shortest: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val pretty: Proof.context -> T -> string -> Pretty.T
- val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
+ val completion: Context.generic -> T -> (string -> bool) -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
val get_scopes: naming -> Binding.scope list
@@ -257,7 +257,7 @@
(* completion *)
-fun completion context space (xname, pos) =
+fun completion context space pred (xname, pos) =
Completion.make (xname, pos) (fn completed =>
let
fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) =
@@ -276,7 +276,7 @@
fun complete xname' name =
if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso
- not (is_concealed space name)
+ not (is_concealed space name) andalso pred name
then
let
val xname'' = ext name;
@@ -565,7 +565,7 @@
in ((name, reports), x) end
| NONE =>
let
- val completions = map (fn pos => completion context space (xname, pos)) ps;
+ val completions = map (fn pos => completion context space (K true) (xname, pos)) ps;
in
error (undefined space name ^ Position.here_list ps ^
Markup.markup_report (implode (map Completion.reported_text completions)))