exit: pass interactive flag, toplevel result convention;
authorwenzelm
Wed Oct 11 22:55:18 2006 +0200 (2006-10-11)
changeset 20981c4d3fc6e1e64
parent 20980 e4fd72aecd03
child 20982 fade54fde622
exit: pass interactive flag, toplevel result convention;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Oct 11 22:55:17 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Oct 11 22:55:18 2006 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
     1.5    val init: string option -> operations -> Proof.context -> local_theory
     1.6    val reinit: local_theory -> local_theory
     1.7 -  val exit: local_theory -> Proof.context
     1.8 +  val exit: bool -> local_theory -> Proof.context * theory
     1.9  end;
    1.10  
    1.11  structure LocalTheory: LOCAL_THEORY =
    1.12 @@ -58,7 +58,7 @@
    1.13      (bstring * thm list) list * local_theory,
    1.14    term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory,
    1.15    declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory,
    1.16 -  exit: local_theory -> local_theory};
    1.17 +  exit: bool -> local_theory -> local_theory};
    1.18  
    1.19  datatype lthy = LThy of
    1.20   {theory_prefix: string option,
    1.21 @@ -169,6 +169,8 @@
    1.22    let val {theory_prefix, operations, target} = get_lthy lthy
    1.23    in init theory_prefix operations target end;
    1.24  
    1.25 -fun exit lthy = lthy |> operation #exit |> target_of;
    1.26 +fun exit int lthy = lthy
    1.27 +  |> operation1 #exit int |> target_of
    1.28 +  |> (fn ctxt => (ctxt, ProofContext.theory_of ctxt));
    1.29  
    1.30  end;