exit: pass interactive flag;
authorwenzelm
Wed Oct 11 22:55:21 2006 +0200 (2006-10-11)
changeset 20984d09f388fa9db
parent 20983 d4500b9b220e
child 20985 de13e2a23c8e
exit: pass interactive flag;
moved exit to local_theory.ML;
tuned pretty;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 11 22:55:20 2006 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 11 22:55:21 2006 +0200
     1.3 @@ -10,9 +10,7 @@
     1.4    val begin: bstring -> Proof.context -> local_theory
     1.5    val init: xstring option -> theory -> local_theory
     1.6    val init_i: string option -> theory -> local_theory
     1.7 -  val exit: local_theory -> Proof.context * theory
     1.8 -  val mapping: xstring option -> (local_theory -> local_theory) ->
     1.9 -    theory -> Proof.context * theory
    1.10 +  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory
    1.11  end;
    1.12  
    1.13  structure TheoryTarget: THEORY_TARGET =
    1.14 @@ -31,14 +29,14 @@
    1.15        (if null fixes then [] else [Element.Fixes fixes]) @
    1.16        (if null assumes then [] else [Element.Assumes assumes]);
    1.17    in
    1.18 -    [Pretty.block
    1.19 -      [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    1.20 -        Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] @
    1.21 -      (if loc = "" then []
    1.22 -       else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
    1.23 -       else
    1.24 -         [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
    1.25 -           (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)])
    1.26 +    if loc = "" then
    1.27 +      [Pretty.block
    1.28 +        [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    1.29 +          Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]
    1.30 +    else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
    1.31 +    else
    1.32 +      [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
    1.33 +        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
    1.34    end;
    1.35  
    1.36  
    1.37 @@ -93,6 +91,7 @@
    1.38        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.39    in
    1.40      lthy
    1.41 +    |> fold (fold Variable.declare_term o snd) specs
    1.42      |> LocalTheory.theory_result (fold_map axiom specs)
    1.43      |-> LocalTheory.notes
    1.44    end;
    1.45 @@ -199,15 +198,13 @@
    1.46      notes = notes loc,
    1.47      term_syntax = term_syntax loc,
    1.48      declaration = declaration loc,
    1.49 -    exit = I};
    1.50 +    exit = K I};
    1.51  
    1.52  fun init_i NONE thy = begin "" (ProofContext.init thy)
    1.53    | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
    1.54  
    1.55  fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
    1.56  
    1.57 -val exit = LocalTheory.exit #> (fn lthy => (lthy, ProofContext.theory_of lthy));
    1.58 -
    1.59 -fun mapping loc f = init loc #> f #> exit;
    1.60 +fun mapping loc f = init loc #> f #> LocalTheory.exit false;
    1.61  
    1.62  end;