# HG changeset patch
# User wenzelm
# Date 1540474900 -7200
# Node ID 6f79d6a5acadd792a2101207f922253b3a9f5cd6
# Parent  4314145005769736a30b68a02c9c229678426d0c
proper completion for @{named_theorems};

diff -r 431414500576 -r 6f79d6a5acad src/Pure/General/name_space.ML
--- 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)))
diff -r 431414500576 -r 6f79d6a5acad src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Oct 25 14:04:37 2018 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Oct 25 15:41:40 2018 +0200
@@ -451,7 +451,7 @@
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
           Markup.markup_report (Completion.reported_text
-            (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
+            (Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos))));
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
@@ -535,7 +535,7 @@
 
 fun consts_completion_message ctxt (c, ps) =
   ps |> map (fn pos =>
-    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)
     |> Completion.reported_text)
   |> implode
   |> Markup.markup_report;
diff -r 431414500576 -r 6f79d6a5acad src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Thu Oct 25 14:04:37 2018 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Thu Oct 25 15:41:40 2018 +0200
@@ -38,6 +38,8 @@
 
 fun undeclared name = "Undeclared named theorems " ^ quote name;
 
+val defined_entry = Symtab.defined o Data.get;
+
 fun the_entry context name =
   (case Symtab.lookup (Data.get context) name of
     NONE => error (undeclared name)
@@ -71,10 +73,17 @@
   let
     val context = Context.Proof ctxt;
     val fact_ref = Facts.Named ((xname, Position.none), NONE);
-    fun err () = error (undeclared xname ^ Position.here pos);
+    fun err () =
+      let
+        val space = Facts.space_of (Proof_Context.facts_of ctxt);
+        val completion = Name_Space.completion context space (defined_entry context) (xname, pos);
+      in
+        error (undeclared xname ^ Position.here pos ^
+          Markup.markup_report (Completion.reported_text completion))
+      end;
   in
     (case try (Proof_Context.get_fact_generic context) fact_ref of
-      SOME (SOME name, _) => if can (the_entry context) name then name else err ()
+      SOME (SOME name, _) => if defined_entry context name then name else err ()
     | _ => err ())
   end;