src/Pure/Isar/proof.ML
changeset 56933 b47193851dc6
parent 56932 11a4001b06c6
child 57486 2131b6633529
equal deleted inserted replaced
56932:11a4001b06c6 56933:b47193851dc6
  1062       if ! testing then ()
  1062       if ! testing then ()
  1063       else Proof_Display.print_results int pos ctxt res;
  1063       else Proof_Display.print_results int pos ctxt res;
  1064     fun print_rule ctxt th =
  1064     fun print_rule ctxt th =
  1065       if ! testing then rule := SOME th
  1065       if ! testing then rule := SOME th
  1066       else if int then
  1066       else if int then
  1067         writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
  1067         Proof_Display.string_of_rule ctxt "Successful" th
       
  1068         |> Markup.markup Markup.text_fold
       
  1069         |> Markup.markup Markup.state
       
  1070         |> writeln
  1068       else ();
  1071       else ();
  1069     val test_proof =
  1072     val test_proof =
  1070       local_skip_proof true
  1073       local_skip_proof true
  1071       |> Unsynchronized.setmp testing true
  1074       |> Unsynchronized.setmp testing true
  1072       |> Exn.interruptible_capture;
  1075       |> Exn.interruptible_capture;