replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
authorwenzelm
Wed Jul 21 15:31:38 2010 +0200 (2010-07-21)
changeset 37871c7ce7685e087
parent 37870 dd9cfc512b7f
child 37872 d83659570337
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
src/Pure/Thy/thy_info.ML
src/Pure/context.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:23:46 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:31:38 2010 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4    val if_known_thy: (string -> unit) -> string -> unit
     1.5    val lookup_theory: string -> theory option
     1.6    val get_theory: string -> theory
     1.7 -  val the_theory: string -> theory -> theory
     1.8    val is_finished: string -> bool
     1.9    val master_directory: string -> Path.T
    1.10    val loaded_files: string -> Path.T list
    1.11 @@ -176,10 +175,6 @@
    1.12      SOME theory => theory
    1.13    | _ => error (loader_msg "undefined theory entry for" [name]));
    1.14  
    1.15 -fun the_theory name thy =
    1.16 -  if Context.theory_name thy = name then thy
    1.17 -  else get_theory name;
    1.18 -
    1.19  
    1.20  
    1.21  (** thy operations **)
     2.1 --- a/src/Pure/context.ML	Wed Jul 21 15:23:46 2010 +0200
     2.2 +++ b/src/Pure/context.ML	Wed Jul 21 15:31:38 2010 +0200
     2.3 @@ -41,6 +41,7 @@
     2.4    val pretty_abbrev_thy: theory -> Pretty.T
     2.5    val str_of_thy: theory -> string
     2.6    val get_theory: theory -> string -> theory
     2.7 +  val this_theory: theory -> string -> theory
     2.8    val deref: theory_ref -> theory
     2.9    val check_thy: theory -> theory_ref
    2.10    val eq_thy: theory * theory -> bool
    2.11 @@ -253,6 +254,10 @@
    2.12    else if #stage (history_of thy) = finished then thy
    2.13    else error ("Unfinished theory " ^ quote name);
    2.14  
    2.15 +fun this_theory thy name =
    2.16 +  if theory_name thy = name then thy
    2.17 +  else get_theory thy name;
    2.18 +
    2.19  
    2.20  (* theory references *)
    2.21  
     3.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:23:46 2010 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:31:38 2010 +0200
     3.3 @@ -910,7 +910,7 @@
     3.4      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     3.5      fun read_const_expr "*" = ([], consts_of thy)
     3.6        | read_const_expr s = if String.isSuffix ".*" s
     3.7 -          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
     3.8 +          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
     3.9            else ([Code.read_const thy s], []);
    3.10    in pairself flat o split_list o map read_const_expr end;
    3.11