src/Pure/Isar/toplevel.ML
changeset 37858 e1ef6b441fe7
parent 37856 173974e07dea
child 37859 575a14dd4167
equal deleted inserted replaced
37857:4e4b8c0dc766 37858:e1ef6b441fe7
    22   val proof_of: state -> Proof.state
    22   val proof_of: state -> Proof.state
    23   val proof_position_of: state -> int
    23   val proof_position_of: state -> int
    24   val enter_proof_body: state -> Proof.state
    24   val enter_proof_body: state -> Proof.state
    25   val print_state_context: state -> unit
    25   val print_state_context: state -> unit
    26   val print_state: bool -> state -> unit
    26   val print_state: bool -> state -> unit
       
    27   val pretty_abstract: state -> Pretty.T
    27   val quiet: bool Unsynchronized.ref
    28   val quiet: bool Unsynchronized.ref
    28   val debug: bool Unsynchronized.ref
    29   val debug: bool Unsynchronized.ref
    29   val interact: bool Unsynchronized.ref
    30   val interact: bool Unsynchronized.ref
    30   val timing: bool Unsynchronized.ref
    31   val timing: bool Unsynchronized.ref
    31   val profiling: int Unsynchronized.ref
    32   val profiling: int Unsynchronized.ref
   210   | SOME (Proof (prf, _)) =>
   211   | SOME (Proof (prf, _)) =>
   211       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   212       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   212   | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
   213   | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
   213   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
   214   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
   214 
   215 
       
   216 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
       
   217 
   215 
   218 
   216 
   219 
   217 (** toplevel transitions **)
   220 (** toplevel transitions **)
   218 
   221 
   219 val quiet = Unsynchronized.ref false;
   222 val quiet = Unsynchronized.ref false;