improved theory, context, update_context;
authorwenzelm
Fri Feb 05 21:04:58 1999 +0100 (1999-02-05 ago)
changeset 62460aa2e536bc20
parent 6245 ebce4ebba491
child 6247 e8bbe64861b8
improved theory, context, update_context;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:04:31 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:04:58 1999 +0100
     1.3 @@ -57,9 +57,10 @@
     1.4    val print_ast_translation: string -> theory -> theory
     1.5    val token_translation: string -> theory -> theory
     1.6    val add_oracle: bstring * string -> theory -> theory
     1.7 -  val the_theory: string -> unit -> theory
     1.8 -  val begin_theory: string * string list -> unit -> theory
     1.9 -  val end_theory: theory -> unit
    1.10 +  val theory: string * string list * (string * bool) list
    1.11 +    -> Toplevel.transition -> Toplevel.transition
    1.12 +  val context: string -> Toplevel.transition -> Toplevel.transition
    1.13 +  val update_context: string -> Toplevel.transition -> Toplevel.transition
    1.14  end;
    1.15  
    1.16  structure IsarThy: ISAR_THY =
    1.17 @@ -239,9 +240,9 @@
    1.18  
    1.19  (* theory init and exit *)
    1.20  
    1.21 -fun the_theory name () = ThyInfo.theory name;
    1.22 -
    1.23 -fun begin_theory (name, names) () = ThyInfo.begin_theory name names;
    1.24 +fun begin_theory (name, parents, files) () =
    1.25 +  let val thy = ThyInfo.begin_theory name parents
    1.26 +  in seq ThyInfo.use (mapfilter (fn (x, true) => Some x | _ => None) files); thy end;
    1.27  
    1.28  fun end_theory thy =
    1.29    let val thy' = PureThy.end_theory thy in
    1.30 @@ -249,5 +250,17 @@
    1.31        handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
    1.32    end;
    1.33  
    1.34 +fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
    1.35 +
    1.36 +
    1.37 +(* context switch *)
    1.38 +
    1.39 +fun switch_theory require name =
    1.40 +  Toplevel.init_theory
    1.41 +    (fn () => (Context.save require name; ThyInfo.get_theory name)) (K ());
    1.42 +
    1.43 +val context = switch_theory ThyInfo.use_thy;
    1.44 +val update_context = switch_theory ThyInfo.update_thy;
    1.45 +
    1.46  
    1.47  end;