src/Pure/Isar/toplevel.ML
changeset 27583 9109f0d8a565
parent 27576 7afff36043e6
child 27601 6683cdb94af8
equal deleted inserted replaced
27582:367aff8d7ffd 27583:9109f0d8a565
    36   val interact: bool ref
    36   val interact: bool ref
    37   val timing: bool ref
    37   val timing: bool ref
    38   val profiling: int ref
    38   val profiling: int ref
    39   val skip_proofs: bool ref
    39   val skip_proofs: bool ref
    40   exception TERMINATE
    40   exception TERMINATE
       
    41   exception EXCURSION_FAIL of exn * string
       
    42   exception TOPLEVEL_ERROR
    41   exception CONTEXT of Proof.context * exn
    43   exception CONTEXT of Proof.context * exn
    42   exception TOPLEVEL_ERROR
       
    43   val exn_message: exn -> string
    44   val exn_message: exn -> string
    44   val program: (unit -> 'a) -> 'a
    45   val program: (unit -> 'a) -> 'a
    45   type transition
    46   type transition
    46   val empty: transition
    47   val empty: transition
    47   val init_of: transition -> string option
    48   val init_of: transition -> string option