check fact names with PIDE markup;
authorwenzelm
Sun Mar 09 17:02:18 2014 +0100 (2014-03-09)
changeset 56003eccac152ffb4
parent 56002 2028467b4df4
child 56004 0364adabdc7b
check fact names with PIDE markup;
src/Pure/facts.ML
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/facts.ML	Sun Mar 09 16:37:56 2014 +0100
     1.2 +++ b/src/Pure/facts.ML	Sun Mar 09 17:02:18 2014 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val empty: T
     1.5    val space_of: T -> Name_Space.T
     1.6    val is_concealed: T -> string -> bool
     1.7 +  val check: Context.generic -> T -> xstring * Position.T -> string
     1.8    val intern: T -> xstring -> string
     1.9    val extern: Proof.context -> T -> string -> xstring
    1.10    val lookup: Context.generic -> T -> string -> (bool * thm list) option
    1.11 @@ -147,6 +148,15 @@
    1.12  
    1.13  val is_concealed = Name_Space.is_concealed o space_of;
    1.14  
    1.15 +fun check context facts (xname, pos) =
    1.16 +  let
    1.17 +    val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
    1.18 +    val _ =
    1.19 +      (case fact of
    1.20 +        Static _ => ()
    1.21 +      | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
    1.22 +  in name end;
    1.23 +
    1.24  val intern = Name_Space.intern o space_of;
    1.25  fun extern ctxt = Name_Space.extern ctxt o space_of;
    1.26  
     2.1 --- a/src/Pure/global_theory.ML	Sun Mar 09 16:37:56 2014 +0100
     2.2 +++ b/src/Pure/global_theory.ML	Sun Mar 09 17:02:18 2014 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  signature GLOBAL_THEORY =
     2.5  sig
     2.6    val facts_of: theory -> Facts.T
     2.7 +  val check_fact: theory -> xstring * Position.T -> string
     2.8    val intern_fact: theory -> xstring -> string
     2.9    val defined_fact: theory -> string -> bool
    2.10    val hide_fact: bool -> string -> theory -> theory
    2.11 @@ -56,6 +57,7 @@
    2.12  
    2.13  val facts_of = Data.get;
    2.14  
    2.15 +fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
    2.16  val intern_fact = Facts.intern o facts_of;
    2.17  val defined_fact = Facts.defined o facts_of;
    2.18