added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
authorwenzelm
Wed Jul 21 14:27:05 2010 +0200 (2010-07-21)
changeset 37867b9783e9e96e1
parent 37866 cd1d1bc7684c
child 37868 59eed00bfd8e
added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Jul 21 13:55:44 2010 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jul 21 14:27:05 2010 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    val string_of_thy: theory -> string
     1.5    val pretty_abbrev_thy: theory -> Pretty.T
     1.6    val str_of_thy: theory -> string
     1.7 +  val get_theory: theory -> string -> theory
     1.8    val deref: theory_ref -> theory
     1.9    val check_thy: theory -> theory_ref
    1.10    val eq_thy: theory * theory -> bool
    1.11 @@ -244,6 +245,14 @@
    1.12  
    1.13  val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
    1.14  
    1.15 +fun get_theory thy name =
    1.16 +  if theory_name thy <> name then
    1.17 +    (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
    1.18 +      SOME thy' => thy'
    1.19 +    | NONE => error ("Unknown ancestor theory " ^ quote name))
    1.20 +  else if #stage (history_of thy) = finished then thy
    1.21 +  else error ("Unfinished theory " ^ quote name);
    1.22 +
    1.23  
    1.24  (* theory references *)
    1.25