src/Pure/Isar/theory_target.ML
changeset 20962 e404275bff33
parent 20915 dcb0a3e2f1bd
child 20984 d09f388fa9db
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 11 00:27:35 2006 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 11 00:27:37 2006 +0200
     1.3 @@ -7,10 +7,12 @@
     1.4  
     1.5  signature THEORY_TARGET =
     1.6  sig
     1.7 +  val begin: bstring -> Proof.context -> local_theory
     1.8    val init: xstring option -> theory -> local_theory
     1.9    val init_i: string option -> theory -> local_theory
    1.10    val exit: local_theory -> Proof.context * theory
    1.11 -  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory
    1.12 +  val mapping: xstring option -> (local_theory -> local_theory) ->
    1.13 +    theory -> Proof.context * theory
    1.14  end;
    1.15  
    1.16  structure TheoryTarget: THEORY_TARGET =
    1.17 @@ -29,15 +31,14 @@
    1.18        (if null fixes then [] else [Element.Fixes fixes]) @
    1.19        (if null assumes then [] else [Element.Assumes assumes]);
    1.20    in
    1.21 -    ([Pretty.block
    1.22 +    [Pretty.block
    1.23        [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    1.24          Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] @
    1.25        (if loc = "" then []
    1.26         else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
    1.27         else
    1.28           [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
    1.29 -           (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]))
    1.30 -    |> Pretty.chunks
    1.31 +           (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)])
    1.32    end;
    1.33  
    1.34  
    1.35 @@ -189,19 +190,19 @@
    1.36  
    1.37  (* init and exit *)
    1.38  
    1.39 -fun target_operations loc exit : LocalTheory.operations =
    1.40 - {pretty = pretty loc,
    1.41 -  consts = consts loc,
    1.42 -  axioms = axioms,
    1.43 -  defs = defs,
    1.44 -  notes = notes loc,
    1.45 -  term_syntax = term_syntax loc,
    1.46 -  declaration = declaration loc,
    1.47 -  exit = exit};
    1.48 +fun begin loc =
    1.49 +  LocalTheory.init (SOME (NameSpace.base loc))
    1.50 +   {pretty = pretty loc,
    1.51 +    consts = consts loc,
    1.52 +    axioms = axioms,
    1.53 +    defs = defs,
    1.54 +    notes = notes loc,
    1.55 +    term_syntax = term_syntax loc,
    1.56 +    declaration = declaration loc,
    1.57 +    exit = I};
    1.58  
    1.59 -fun init_i NONE thy = LocalTheory.init (SOME "") (target_operations "" I) (ProofContext.init thy)
    1.60 -  | init_i (SOME loc) thy =
    1.61 -      LocalTheory.init (SOME (NameSpace.base loc)) (target_operations loc I) (Locale.init loc thy);
    1.62 +fun init_i NONE thy = begin "" (ProofContext.init thy)
    1.63 +  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
    1.64  
    1.65  fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
    1.66