src/Pure/Isar/toplevel.ML
changeset 29380 a9ee3475abf4
parent 29343 43ac99cdeb5b
child 29386 d5849935560c
equal deleted inserted replaced
29379:f65670092259 29380:a9ee3475abf4
     1 (*  Title:      Pure/Isar/toplevel.ML
     1 (*  Title:      Pure/Isar/toplevel.ML
     2     ID:         $Id$
       
     3     Author:     Markus Wenzel, TU Muenchen
     2     Author:     Markus Wenzel, TU Muenchen
     4 
     3 
     5 Isabelle/Isar toplevel transactions.
     4 Isabelle/Isar toplevel transactions.
     6 *)
     5 *)
     7 
     6 
    64   val theory: (theory -> theory) -> transition -> transition
    63   val theory: (theory -> theory) -> transition -> transition
    65   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    64   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    66   val theory': (bool -> theory -> theory) -> transition -> transition
    65   val theory': (bool -> theory -> theory) -> transition -> transition
    67   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    66   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    68   val end_local_theory: transition -> transition
    67   val end_local_theory: transition -> transition
       
    68   val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
       
    69     transition -> transition
    69   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
    70   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
    70   val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
    71   val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
    71   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
    72   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
    72     transition -> transition
    73     transition -> transition
    73   val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
    74   val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
   510 
   511 
   511 fun local_theory_presentation loc f g = transaction (fn int =>
   512 fun local_theory_presentation loc f g = transaction (fn int =>
   512   (fn Theory (gthy, _) =>
   513   (fn Theory (gthy, _) =>
   513         let
   514         let
   514           val finish = loc_finish loc gthy;
   515           val finish = loc_finish loc gthy;
   515           val lthy' = f (loc_begin loc gthy);
   516           val lthy' = f int (loc_begin loc gthy);
   516         in Theory (finish lthy', SOME lthy') end
   517         in Theory (finish lthy', SOME lthy') end
   517     | _ => raise UNDEF) #> tap g);
   518     | _ => raise UNDEF) #> tap g);
   518 
   519 
   519 in
   520 in
   520 
   521 
   521 fun local_theory loc f = local_theory_presentation loc f (K I);
   522 fun local_theory' loc f = local_theory_presentation loc f (K I);
   522 fun present_local_theory loc g = local_theory_presentation loc I g;
   523 fun local_theory loc f = local_theory' loc (K f);
       
   524 fun present_local_theory loc g = local_theory_presentation loc (K I) g;
   523 
   525 
   524 end;
   526 end;
   525 
   527 
   526 
   528 
   527 (* proof transitions *)
   529 (* proof transitions *)