src/Pure/Isar/toplevel.ML
changeset 50201 c26369c9eda6
parent 49863 b5fb6e7f8d81
child 50739 5165d7e6d3b9
equal deleted inserted replaced
50200:2c94c065564e 50201:c26369c9eda6
   209     NONE => []
   209     NONE => []
   210   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   210   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   211   | SOME (Proof (prf, _)) =>
   211   | SOME (Proof (prf, _)) =>
   212       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   212       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   213   | 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)])
   214   |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln;
   214   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
   215 
   215 
   216 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
   216 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
   217 
   217 
   218 
   218 
   219 
   219