begin/end_theory: presentation;
authorwenzelm
Tue Mar 09 12:20:04 1999 +0100 (1999-03-09)
changeset 6331fb7b8d6c2bd1
parent 6330 e1faf0f6f2b8
child 6332 7cee353c7f2a
begin/end_theory: presentation;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Mar 09 12:19:25 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Mar 09 12:20:04 1999 +0100
     1.3 @@ -57,6 +57,8 @@
     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 begin_theory: string -> string list -> (string * bool) list -> theory
     1.8 +  val end_theory: theory -> theory
     1.9    val theory: string * string list * (string * bool) list
    1.10      -> Toplevel.transition -> Toplevel.transition
    1.11    val context: string -> Toplevel.transition -> Toplevel.transition
    1.12 @@ -174,8 +176,8 @@
    1.13  
    1.14  (* use ML text *)
    1.15  
    1.16 -fun use_mltext txt opt_thy = #2 (Context.fetch opt_thy (use_text false) txt);
    1.17 -fun use_mltext_theory txt thy = #2 (Context.fetch_theory thy (use_text false) txt);
    1.18 +fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);
    1.19 +fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);
    1.20  
    1.21  fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
    1.22  
    1.23 @@ -222,21 +224,31 @@
    1.24      ("(" ^ quote name ^ ", " ^ txt ^ ")");
    1.25  
    1.26  
    1.27 -(* theory init and exit *)
    1.28 +(* theory init and exit *)	(* FIXME move? rearrange? *)
    1.29  
    1.30 -fun begin_theory (name, parents, files) () =
    1.31 +fun begin_theory name parents files =
    1.32    let
    1.33 -    val thy = ThyInfo.begin_theory name parents;
    1.34 -    val names = mapfilter (fn (x, true) => Some x | _ => None) files;
    1.35 -  in Context.setmp (Some thy) (seq ThyInfo.use) names; thy end;
    1.36 +    val paths = map (apfst Path.unpack) files;
    1.37 +    val thy = ThyInfo.begin_theory name parents paths;
    1.38 +  in Present.begin_theory name parents paths; thy end;
    1.39  
    1.40 +
    1.41 +(* FIXME
    1.42  fun end_theory thy =
    1.43    let val thy' = PureThy.end_theory thy in
    1.44 +    Present.end_theory (PureThy.get_name thy');
    1.45      transform_error ThyInfo.put_theory thy'
    1.46        handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
    1.47    end;
    1.48 +*)
    1.49  
    1.50 -fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
    1.51 +fun end_theory thy =
    1.52 +  (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
    1.53 +
    1.54 +fun bg_theory (name, parents, files) () = begin_theory name parents files;
    1.55 +fun en_theory thy = (end_theory thy; ());
    1.56 +
    1.57 +fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory;
    1.58  
    1.59  
    1.60  (* context switch *)