check fact names with PIDE markup;

--- a/src/Pure/facts.ML	Sun Mar 09 16:37:56 2014 +0100
+++ b/src/Pure/facts.ML	Sun Mar 09 17:02:18 2014 +0100
@@ -23,6 +23,7 @@
   val empty: T
   val space_of: T -> Name_Space.T
   val is_concealed: T -> string -> bool
+  val check: Context.generic -> T -> xstring * Position.T -> string
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
@@ -147,6 +148,15 @@
 
 val is_concealed = Name_Space.is_concealed o space_of;
 
+fun check context facts (xname, pos) =
+  let
+    val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
+    val _ =
+      (case fact of
+        Static _ => ()
+      | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
+  in name end;
+
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
 

--- a/src/Pure/global_theory.ML	Sun Mar 09 16:37:56 2014 +0100
+++ b/src/Pure/global_theory.ML	Sun Mar 09 17:02:18 2014 +0100
@@ -7,6 +7,7 @@
 signature GLOBAL_THEORY =
 sig
   val facts_of: theory -> Facts.T
+  val check_fact: theory -> xstring * Position.T -> string
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
@@ -56,6 +57,7 @@
 
 val facts_of = Data.get;
 
+fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;