tuned
authorhaftmann
Wed Aug 11 15:45:15 2010 +0200 (2010-08-11 ago)
changeset 383780b6fa86110e7
parent 38377 2dfd8b7b8274
child 38379 67d71449e85b
tuned
src/Pure/Isar/named_target.ML
     1.1 --- a/src/Pure/Isar/named_target.ML	Wed Aug 11 15:09:31 2010 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 15:45:15 2010 +0200
     1.3 @@ -22,7 +22,13 @@
     1.4  fun make_target target is_locale is_class =
     1.5    Target {target = target, is_locale = is_locale, is_class = is_class};
     1.6  
     1.7 -val global_target = make_target "" false false;
     1.8 +val global_target = Target {target = "", is_locale = false, is_class = false};
     1.9 +
    1.10 +fun named_target _ NONE = global_target
    1.11 +  | named_target thy (SOME locale) =
    1.12 +      if Locale.defined thy locale
    1.13 +      then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale}
    1.14 +      else error ("No such locale: " ^ quote locale);
    1.15  
    1.16  structure Data = Proof_Data
    1.17  (
    1.18 @@ -168,18 +174,18 @@
    1.19      pretty_thy ctxt target is_class;
    1.20  
    1.21  
    1.22 -(* init various targets *)
    1.23 +(* init *)
    1.24  
    1.25  local
    1.26  
    1.27 -fun init_data (Target {target, is_locale, is_class}) =
    1.28 +fun init_context (Target {target, is_locale, is_class}) =
    1.29    if not is_locale then ProofContext.init_global
    1.30    else if not is_class then Locale.init target
    1.31    else Class_Target.init target;
    1.32  
    1.33  fun init_target (ta as Target {target, ...}) thy =
    1.34    thy
    1.35 -  |> init_data ta
    1.36 +  |> init_context ta
    1.37    |> Data.put ta
    1.38    |> Local_Theory.init NONE (Long_Name.base_name target)
    1.39       {define = Generic_Target.define (target_foundation ta),
    1.40 @@ -193,12 +199,6 @@
    1.41        reinit = init_target ta o ProofContext.theory_of,
    1.42        exit = Local_Theory.target_of};
    1.43  
    1.44 -fun named_target _ NONE = global_target
    1.45 -  | named_target thy (SOME target) =
    1.46 -      if Locale.defined thy target
    1.47 -      then make_target target true (Class_Target.is_class thy target)
    1.48 -      else error ("No such locale: " ^ quote target);
    1.49 -
    1.50  in
    1.51  
    1.52  fun init target thy = init_target (named_target thy target) thy;