src/Pure/Isar/toplevel.ML
changeset 9512 c30f6d0f81d2
parent 9453 4b37161f2b2e
child 10324 498999fd7c37
equal deleted inserted replaced
9511:bb029080ff8b 9512:c30f6d0f81d2
    51   val theory': (bool -> theory -> theory) -> transition -> transition
    51   val theory': (bool -> theory -> theory) -> transition -> transition
    52   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    52   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    53   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    53   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    54   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    54   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    55   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    55   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
       
    56   val unknown_theory: transition -> transition
       
    57   val unknown_proof: transition -> transition
       
    58   val unknown_context: transition -> transition
    56   val quiet: bool ref
    59   val quiet: bool ref
    57   val exn_message: exn -> string
    60   val exn_message: exn -> string
    58   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    61   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    59   val excursion_result: ((transition * (state -> 'a -> 'a)) list * 'a) -> 'a
    62   val excursion_result: ((transition * (state -> 'a -> 'a)) list * 'a) -> 'a
    60   val excursion: transition list -> unit
    63   val excursion: transition list -> unit
   344 fun theory_to_proof f =
   347 fun theory_to_proof f =
   345   app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
   348   app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
   346 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
   349 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
   347 val proof = proof' o K;
   350 val proof = proof' o K;
   348 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
   351 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
       
   352 
       
   353 val unknown_theory = imperative (fn () => warning "Unknown theory context");
       
   354 val unknown_proof = imperative (fn () => warning "Unknown proof context");
       
   355 val unknown_context = imperative (fn () => warning "Unknown context");
   349 
   356 
   350 
   357 
   351 
   358 
   352 (** toplevel transactions **)
   359 (** toplevel transactions **)
   353 
   360