# HG changeset patch # User wenzelm # Date 1163193533 -3600 # Node ID 5f5162f40ac70d1dc65191c5ed106f6d9883d7ce # Parent 11143b6ad87fd2eeed4c08666064a2d3a8c2f980 removed mapping; added reinit; diff -r 11143b6ad87f -r 5f5162f40ac7 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 10 22:18:52 2006 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 10 22:18:53 2006 +0100 @@ -11,7 +11,6 @@ val begin: bstring -> Proof.context -> local_theory val init: xstring option -> theory -> local_theory val init_i: string option -> theory -> local_theory - val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory end; structure TheoryTarget: THEORY_TARGET = @@ -201,21 +200,20 @@ | declaration loc f = I; (* FIXME *) - (* init and exit *) -fun begin loc ctxt = ctxt - |> Data.put (if loc = "" then NONE else SOME loc) - |> LocalTheory.init (SOME (NameSpace.base loc)) - {pretty = pretty loc, - consts = consts loc, - axioms = axioms, - defs = defs, - notes = notes loc, - term_syntax = term_syntax loc, - declaration = declaration loc, - reinit = begin loc, - exit = K I}; +fun begin loc = + Data.put (if loc = "" then NONE else SOME loc) #> + LocalTheory.init (SOME (NameSpace.base loc)) + {pretty = pretty loc, + consts = consts loc, + axioms = axioms, + defs = defs, + notes = notes loc, + term_syntax = term_syntax loc, + declaration = declaration loc, + reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc), + exit = LocalTheory.target_of} fun init_i NONE thy = begin "" (ProofContext.init thy) | init_i (SOME loc) thy = begin loc (Locale.init loc thy); @@ -223,6 +221,4 @@ fun init (SOME "-") thy = init_i NONE thy | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; -fun mapping loc f = init loc #> f #> LocalTheory.exit false; - end;