src/Pure/Isar/named_target.ML
changeset 41585 45d7da4e4ccf
parent 40782 aa533c5e3f48
child 41959 b460124855b8
     1.1 --- a/src/Pure/Isar/named_target.ML	Sat Jan 15 22:40:17 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sun Jan 16 14:57:14 2011 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature NAMED_TARGET =
     1.6  sig
     1.7 -  val init: string -> theory -> local_theory
     1.8 +  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
     1.9    val theory_init: theory -> local_theory
    1.10    val reinit: local_theory -> local_theory -> local_theory
    1.11    val context_cmd: xstring -> theory -> local_theory
    1.12 @@ -19,12 +19,18 @@
    1.13  
    1.14  (* context data *)
    1.15  
    1.16 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    1.17 +datatype target =
    1.18 +  Target of {target: string, is_locale: bool, is_class: bool,
    1.19 +    before_exit: local_theory -> local_theory};
    1.20  
    1.21 -fun named_target _ "" = Target {target = "", is_locale = false, is_class = false}
    1.22 -  | named_target thy locale =
    1.23 +fun make_target target is_locale is_class before_exit =
    1.24 +  Target {target = target, is_locale = is_locale, is_class = is_class,
    1.25 +    before_exit = before_exit};
    1.26 +
    1.27 +fun named_target _ "" before_exit = make_target "" false false before_exit
    1.28 +  | named_target thy locale before_exit =
    1.29        if Locale.defined thy locale
    1.30 -      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
    1.31 +      then make_target locale true (Class.is_class thy locale) before_exit
    1.32        else error ("No such locale: " ^ quote locale);
    1.33  
    1.34  structure Data = Proof_Data
    1.35 @@ -33,7 +39,9 @@
    1.36    fun init _ = NONE;
    1.37  );
    1.38  
    1.39 -val peek = Option.map (fn Target args => args) o Data.get;
    1.40 +val peek =
    1.41 +  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
    1.42 +    {target = target, is_locale = is_locale, is_class = is_class});
    1.43  
    1.44  
    1.45  (* generic declarations *)
    1.46 @@ -169,14 +177,14 @@
    1.47  
    1.48  (* init *)
    1.49  
    1.50 -fun init_context (Target {target, is_locale, is_class}) =
    1.51 +fun init_context (Target {target, is_locale, is_class, ...}) =
    1.52    if not is_locale then ProofContext.init_global
    1.53    else if not is_class then Locale.init target
    1.54    else Class.init target;
    1.55  
    1.56 -fun init target thy =
    1.57 +fun init before_exit target thy =
    1.58    let
    1.59 -    val ta = named_target thy target;
    1.60 +    val ta = named_target thy target before_exit;
    1.61    in
    1.62      thy
    1.63      |> init_context ta
    1.64 @@ -190,17 +198,17 @@
    1.65          syntax_declaration = fn pervasive => target_declaration ta
    1.66            {syntax = true, pervasive = pervasive},
    1.67          pretty = pretty ta,
    1.68 -        exit = Local_Theory.target_of}
    1.69 +        exit = Local_Theory.target_of o before_exit}
    1.70    end;
    1.71  
    1.72 -val theory_init = init "";
    1.73 +val theory_init = init I "";
    1.74  
    1.75  fun reinit lthy =
    1.76 -  (case peek lthy of
    1.77 -    SOME {target, ...} => init target o Local_Theory.exit_global
    1.78 +  (case Data.get lthy of
    1.79 +    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
    1.80    | NONE => error "Not in a named target");
    1.81  
    1.82 -fun context_cmd "-" thy = init "" thy
    1.83 -  | context_cmd target thy = init (Locale.intern thy target) thy;
    1.84 +fun context_cmd "-" thy = init I "" thy
    1.85 +  | context_cmd target thy = init I (Locale.intern thy target) thy;
    1.86  
    1.87  end;